Martin Blicha 0340510c53 [SMTChecker] correct handling of FixedBytes constants initialized with string literal

2021-03-04 15:14:47 +01:00

..

CHCSmtLib2Interface.cpp

Add const ref to prevent segfaults.

2020-12-04 14:57:46 +01:00

CHCSmtLib2Interface.h

Add const ref to prevent segfaults.

2020-12-04 14:57:46 +01:00

CHCSolverInterface.h

[SMTChecker] User timeout option

2020-11-03 10:46:11 +00:00

CMakeLists.txt

Allow loading Z3 dynamically at runtime.

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

CVC4Interface.cpp

Enable the -Wconversion warning

2020-12-08 16:45:24 +00:00

CVC4Interface.h

[SMTChecker] User timeout option

2020-11-03 10:46:11 +00:00

Exceptions.h

Add SPDX license identifier if not present already in source file

2020-07-17 20:24:12 +05:30

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

[SMTChecker] User timeout option

2020-11-03 10:46:11 +00:00

SMTLib2Interface.h

[SMTChecker] User timeout option

2020-11-03 10:46:11 +00:00

SMTPortfolio.cpp

Allow loading Z3 dynamically at runtime.

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

SMTPortfolio.h

[SMTChecker] Avoid implicit conversion

2020-11-11 16:29:03 +00:00

SolverInterface.h

[SMTChecker] correct handling of FixedBytes constants initialized with string literal

2021-03-04 15:14:47 +01:00

Sorts.cpp

Introduce bitvector sort.

2020-09-09 17:26:52 +02:00

Sorts.h

Introduce bitvector sort.

2020-09-09 17:26:52 +02:00

Z3CHCInterface.cpp

Do not request proof for old z3

2020-12-03 20:57:23 +01:00

Z3CHCInterface.h

Do not request proof for old z3

2020-12-03 20:57:23 +01:00

Z3Interface.cpp

Allow loading Z3 dynamically at runtime.

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

Z3Interface.h

Allow loading Z3 dynamically at runtime.

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

Z3Loader.cpp

Allow loading Z3 dynamically at runtime.

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

Z3Loader.h

Allow loading Z3 dynamically at runtime.

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