Martin Blicha
475cfe2532
Ignore standard error output from solvers
2023-09-05 12:39:20 +02:00
Martin Blicha
a4b4e70b67
Get invariants from eldarica
2023-09-05 12:39:20 +02:00
Martin Blicha
d8c1a124e7
Bring back solving with temporary file for Eldarica
2023-09-05 12:39:19 +02:00
Martin Blicha
497ca183b4
Small cleanup
2023-09-05 12:39:19 +02:00
Martin Blicha
1b68b5764d
SMTChecker: Ignore model checking without callback
2023-09-05 12:39:19 +02:00
Martin Blicha
b6326f4d4d
Do not stop reading solver's output after it terminated
2023-09-05 12:39:19 +02:00
Martin Blicha
8e0e2cb1ae
Throw when trying to read past the end of SMTLib stream
2023-09-05 12:39:19 +02:00
Martin Blicha
d3bbc51ee9
Update test after change in variable names
2023-09-05 12:39:19 +02:00
Martin Blicha
4101c67cba
Update to let inlining
2023-09-05 12:39:19 +02:00
Martin Blicha
bbd7ef447f
Updates to command-line tests
2023-09-05 12:39:19 +02:00
Martin Blicha
ec10f46acb
Parse BMC counterexample properly
2023-09-05 12:39:19 +02:00
Martin Blicha
af1acaba64
Refactor SMTLib parser to separate file
2023-09-05 12:39:19 +02:00
Martin Blicha
3a01b432c4
Hack to get around problem in Z3
2023-09-05 12:39:19 +02:00
Martin Blicha
8c99c125c4
Add support for parsing invariants
2023-09-05 12:39:19 +02:00
Martin Blicha
b8f89fa45d
SMTSolverCommand: Use pipe instead of temporary file for the query
2023-09-05 12:39:19 +02:00
Martin Blicha
3f22118bbe
More checks
2023-09-05 12:39:19 +02:00
Martin Blicha
01ed412714
Stronger checks
2023-09-05 12:39:19 +02:00
Martin Blicha
0c13b7ee8f
Turn asserts into solAsserts
2023-09-05 12:39:19 +02:00
Martin Blicha
83b60754a9
Update to the tests to combat nondeterminism
2023-09-05 12:39:19 +02:00
Martin Blicha
342df8a515
Ensure SMT-LIB file is complete
2023-09-05 12:39:19 +02:00
Martin Blicha
5569aaee78
Fix coding style
2023-09-05 12:39:19 +02:00
Martin Blicha
ecded11833
Tests: Disable checking CEX
...
In this case I observed brittle behaviour with Z3, which behaved
differently on two equivalent queries with only variables renamed.
The reason for different versions was that in isoltest, we add version
pragma to the source code and this changes the ids of AST nodes. These
are in turn used to generate uniques names for SMT variables.
2023-09-05 12:39:19 +02:00
Martin Blicha
799f418bef
Make counterexample deterministic
2023-09-05 12:39:19 +02:00
Martin Blicha
4ecaa476fd
Handle custom tuple sorts in a general way
2023-09-05 12:39:19 +02:00
Martin Blicha
742642ebae
Use answer from second Z3 call only when solved
2023-09-05 12:39:19 +02:00
Martin Blicha
0fbeb3a69d
Throw exception on unhandled cases in SMT-LIB Expression conversion
2023-09-05 12:39:19 +02:00
Martin Blicha
4b50f26834
Negative numbers do not have to be atoms
2023-09-05 12:39:19 +02:00
Martin Blicha
779db2d84f
Use shared pointers, not raw pointers, for caching sorts
2023-09-05 12:39:19 +02:00
Martin Blicha
b65c37029d
Fix parsing array expressions from SMT-LIB proof
2023-09-05 12:39:19 +02:00
Martin Blicha
d773e76704
Remove outdated FIXME
2023-09-05 12:39:19 +02:00
Martin Blicha
451b6f8ced
Fix handling of structs in SMT-LIB CEX
2023-09-05 12:39:19 +02:00
Martin Blicha
9339b7074a
Fix parsing of let expression to allow shadowing values
2023-09-05 12:39:19 +02:00
Martin Blicha
92689e4256
Fix code style problems
2023-09-05 12:39:19 +02:00
Martin Blicha
8ea8a1eb99
Cache sorts already in SMTLib2Interface
...
This allows us to ask for a sort of a sort from its string
representation parsed from an SMT-LIB solver response
2023-09-05 12:39:19 +02:00
Martin Blicha
6acbe2ec35
Towards translating proof from SMT-LIB response
2023-09-05 12:39:19 +02:00
Martin Blicha
479bb9c3de
Fix missing std
2023-09-05 12:39:19 +02:00
Martin Blicha
2195b5e57a
Solve UNSAT queries again with proof production enabled
2023-09-05 12:39:19 +02:00
Martin Blicha
c90b48af02
Update to the tests
2023-09-05 12:39:19 +02:00
Martin Blicha
58d0579ba6
SMTCheckerTests: Use SMT callback
2023-09-05 12:39:19 +02:00
Martin Blicha
1d60559551
Use same spacer parameters as before
2023-09-05 12:39:19 +02:00
Martin Blicha
d9dc8f475e
Enable resource limit for Z3
2023-09-05 12:39:19 +02:00
Martin Blicha
c6f274892e
Fix SMTLib2Interface
2023-09-05 12:39:19 +02:00
Martin Blicha
f4b849972c
Remove smtlib2 solver option
2023-09-05 12:39:17 +02:00
Martin Blicha
72974adb92
Fix check for SMT query in UniversalCallback
2023-09-05 12:37:56 +02:00
Martin Blicha
e7fe310bc2
Remove unnecessary header
2023-09-05 12:37:56 +02:00
Martin Blicha
da2f4cb100
Try to parse values only for satisfiable answer
2023-09-05 12:37:56 +02:00
Martin Blicha
efb0d4253c
Use callback properly in SMTLib2 interface
2023-09-05 12:37:56 +02:00
Martin Blicha
cabec89872
Removing SMT portfolio
2023-09-05 12:37:56 +02:00
Martin Blicha
1e190abf6e
Initial work on unified way to interact with solvers
2023-09-05 12:37:56 +02:00
Daniel
16ae76cad7
Merge pull request #14533 from ethereum/fix-std-namespace-asan
...
Fix missing std qualifier for ASAN
2023-09-05 11:04:13 +02:00
Martin Blicha
Daniel