Martin Blicha ec10f46acb Parse BMC counterexample properly

2023-09-05 12:39:19 +02:00

..

CHCSmtLib2Interface.cpp

Refactor SMTLib parser to separate file

2023-09-05 12:39:19 +02:00

CHCSmtLib2Interface.h

Refactor SMTLib parser to separate file

2023-09-05 12:39:19 +02:00

CHCSolverInterface.h

Add invariant to the solver results

2021-10-26 11:30:30 +02:00

CMakeLists.txt

Refactor SMTLib parser to separate file

2023-09-05 12:39:19 +02:00

Exceptions.h

Put arguments in parantheses in assert macro definitions

2022-04-06 22:26:21 +02:00

genz3wrapper.py

Allow loading Z3 dynamically at runtime.

2020-12-10 16:47:47 +01:00

Helpers.h

Small fixes wrt ReasoningBasedSimplifier.

2020-09-16 18:08:54 +02:00

SMTLib2Interface.cpp

Parse BMC counterexample properly

2023-09-05 12:39:19 +02:00

SMTLib2Interface.h

Use shared pointers, not raw pointers, for caching sorts

2023-09-05 12:39:19 +02:00

SMTLibParser.cpp

Refactor SMTLib parser to separate file

2023-09-05 12:39:19 +02:00

SMTLibParser.h

Refactor SMTLib parser to separate file

2023-09-05 12:39:19 +02:00

SolverInterface.h

Remove smtlib2 solver option

2023-09-05 12:39:17 +02:00

Sorts.cpp

Purge using namespace std in libsmtutil and libsolc

2023-07-12 14:09:19 +02:00

Sorts.h

Implement missing overrides and relax smtAsserts

2023-05-09 13:20:56 -03:00