PV1 ⊧ ddSMTminimizes an input that triggers faulty behavior in an SMT solver

Delta-debugger for the SMT-LIBv2 language.

Application domain/field

• Debugging
• SMT solving

Type of tool

Debugger for SMT solvers

Expected input

• Command, a typical command would be a call to an SMT solver.
• Input: SMT problem which can be used to trigger the problem

Format:

One of the following:

• SMT-LIB
• SyGuS
• the separation logic extension for SMT-LIB.

Expected output

Minimal working example, i.e. an input that is as small as possible but still triggers the original faulty behavior of the executed command.

Internals

Delta debugging: the goal is to minimize failure-inducing inputs. It extracts a minimal working example by omitting parts of the input that are irrelevant for triggering the faulty behavior.

Comments

License: GPLv3