Daniel Kirchner
|
cb72d76aaf
|
Add const ref to prevent segfaults.
|
2020-12-04 14:57:46 +01:00 |
|
Leonardo Alt
|
4210e09d9a
|
Do not request proof for old z3
|
2020-12-03 20:57:23 +01:00 |
|
a3d4
|
148c379ab9
|
Fix Visual Studio compilation error (add missing include <optional>)
|
2020-11-16 17:42:51 +01:00 |
|
Alex Beregszaszi
|
2f899bbffa
|
[SMTChecker] Avoid implicit conversion
|
2020-11-11 16:29:03 +00:00 |
|
Leonardo Alt
|
d03ddeb0fa
|
[SMTChecker] User timeout option
|
2020-11-03 10:46:11 +00:00 |
|
Leonardo Alt
|
446e46fe06
|
Use Expression instead of plain strings for counterexamples
|
2020-10-27 12:04:51 +00:00 |
|
Leonardo Alt
|
72b052eae7
|
Convert z3::expr to smtutil::Expression
|
2020-10-27 12:04:51 +00:00 |
|
Leonardo Alt
|
0223571987
|
[SMTChecker] Do not report error when rlimit
|
2020-09-25 18:43:10 +02:00 |
|
Leonardo
|
35a7d5d3e4
|
Merge pull request #9873 from ethereum/smt_dec_rlimit
[SMTChecker] Decrease rlimit
|
2020-09-23 23:11:59 +02:00 |
|
Leonardo Alt
|
ebb6f61506
|
[SMTChecker] Decrease rlimit
|
2020-09-23 19:28:47 +02:00 |
|
Leonardo Alt
|
5917fd82b3
|
[SMTChecker] Do not throw when counterexample is not available (older z3 versions)
|
2020-09-23 19:17:38 +02:00 |
|
chriseth
|
6e2d2feb10
|
Small fixes wrt ReasoningBasedSimplifier.
|
2020-09-16 18:08:54 +02:00 |
|
chriseth
|
f73fb726af
|
Reasoning based optimizer.
|
2020-09-15 15:57:58 +02:00 |
|
Leonardo Alt
|
23ee011c56
|
[SMTChecker] Fix imports
|
2020-09-11 13:34:46 +02:00 |
|
Leonardo Alt
|
40197df104
|
[SMTChecker] Support shifts
|
2020-09-09 19:47:52 +02:00 |
|
chriseth
|
a2cac93cbf
|
Introduce bitvector sort.
|
2020-09-09 17:26:52 +02:00 |
|
Leonardo Alt
|
7ca335adde
|
Decrease rlimit
|
2020-09-01 08:25:07 +02:00 |
|
Djordje Mijovic
|
11a7763f49
|
[SMTChecker] Support bitwise or, xor and not.
|
2020-08-26 11:06:56 +02:00 |
|
Leonardo Alt
|
5bb4e73693
|
Review 1
|
2020-07-23 18:49:03 +02:00 |
|
Leonardo Alt
|
51721c3080
|
Double SAT run for cex
|
2020-07-23 18:49:03 +02:00 |
|
Leonardo Alt
|
744905525f
|
Convert z3 cex graph into STL
|
2020-07-23 18:49:03 +02:00 |
|
Sachin Grover
|
b7adb2aa42
|
Add SPDX license identifier if not present already in source file
Fixes: #9220
|
2020-07-17 20:24:12 +05:30 |
|
Leonardo Alt
|
46653b2d43
|
Fix ICE when bitwise operator on fixed bytes
|
2020-07-15 19:32:15 +02:00 |
|
Djordje Mijovic
|
547590b972
|
Fixing additional signedness errors after adding -Wsign-conversion flag
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
|
2020-07-09 17:22:45 +02:00 |
|
Leonardo Alt
|
27f0529b80
|
[SMTChecker] Decrease Z3 resource limit
|
2020-07-06 11:30:24 +02:00 |
|
Leonardo
|
b9f2697a3c
|
Merge pull request #9094 from ethereum/conversionWarningsSmtUtil
Adding fixes for signedness warnings in smtutil
|
2020-06-03 01:03:44 +02:00 |
|
Djordje Mijovic
|
d2924d83a2
|
Adding fixes for signedness warnings in smtutil
|
2020-06-02 18:49:26 +02:00 |
|
Leonardo Alt
|
9e9f0c52e1
|
[SMTChecker] Support to bitwise
|
2020-05-27 20:59:00 +02:00 |
|
Leonardo Alt
|
25de3975ce
|
Add SMTLogicException
|
2020-05-20 12:55:19 +02:00 |
|
Leonardo Alt
|
7a91c9b971
|
Remove Type from SolverInterface
|
2020-05-20 12:55:19 +02:00 |
|
Leonardo Alt
|
45eba27424
|
Rename namespace
|
2020-05-20 12:55:18 +02:00 |
|
Leonardo Alt
|
802d66244d
|
Do not link unnecessarily
|
2020-05-20 12:55:18 +02:00 |
|
Leonardo Alt
|
087605ea02
|
Create libsmtutil
|
2020-05-20 12:55:18 +02:00 |
|