mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity
11548 commits 24 branches 48 tags 158 MiB
Commit graph

9446 commits

Author SHA1 Message Date
Nikolaj Bjorner
79d4502771 atomics for #2565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-25 20:22:35 -07:00
Nikolaj Bjorner
18fe28c0f0 fix perf bug exposed by Shelly Grossman 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-25 20:01:06 -07:00
Nikolaj Bjorner
3dcfbb8347 fix #2585 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-25 18:57:51 -07:00
Nikolaj Bjorner
2a1f05e7e8 remove Simplify rewrite resulting in flaky build breaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-25 10:11:33 -07:00
Nikolaj Bjorner
20feecc7b0 z3.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-25 09:18:13 -07:00
Nikolaj Bjorner
666a237cbc z3.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-25 09:16:59 -07:00
Nikolaj Bjorner
1b910c4ed2 hash update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-24 18:21:05 -07:00
Nikolaj Bjorner
d0fc463a0c fix #2581 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-24 15:56:53 -07:00
Nikolaj Bjorner
38ad66ce17 update hash #2579 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-24 12:31:30 -07:00
Nikolaj Bjorner
1203af83eb expose cardinality declarations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-24 12:30:25 -07:00
Nikolaj Bjorner
f7cc68aa6a fix #2580 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-24 08:58:36 -07:00
Nikolaj Bjorner
74aa47f458 fix #2578 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-23 13:52:27 -07:00
Nikolaj Bjorner
2dd9ea071d fix #2577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-23 10:41:00 -07:00
Nikolaj Bjorner
64d4e599c1 re rewriter for loop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-23 09:40:23 -07:00
Nikolaj Bjorner
dee8a9f308 remove more unsound rewrites #2575 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-23 02:56:31 -07:00
NikolajBjorner
6b117c0b2c move to zarith #2471 
Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
 2019-09-23 02:46:11 -07:00
Nikolaj Bjorner
0b06a9b5d8 fix minor version numbering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-23 01:57:03 -07:00
Nikolaj Bjorner
a44cf7a9ba unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-22 10:15:20 -07:00
Nikolaj Bjorner
dc625cb01d remove unsound rewrite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-22 08:40:44 -07:00
Nikolaj Bjorner
48e996241e fix initialization order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-20 10:17:27 -07:00
Nikolaj Bjorner
4101652747 handle case where lower bound is above upper 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-20 09:54:18 -07:00
Nikolaj Bjorner
b506e45845 align name of tactic in report 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-20 08:57:21 -07:00
Nikolaj Bjorner
cd0cd82eb7 add rewrites for #2575 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-20 08:55:53 -07:00
Nikolaj Bjorner
12034df11a add rewrites for #2575 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-20 02:16:30 -07:00
Nikolaj Bjorner
f8df7770a2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-19 16:41:28 -07:00
Nikolaj Bjorner
df2f0416e2 undo atomic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-17 21:56:28 -04:00
Nikolaj Bjorner
c68cfe878e #2565 use atomic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-17 18:15:19 -07:00
Nikolaj Bjorner
04ae00048d fix #2567 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-17 18:48:21 -04:00
Nikolaj Bjorner
9c74c05854 address min-int overflow reported in #2565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-17 18:19:55 -04:00
Nikolaj Bjorner
77ef40a3db na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-17 11:50:14 -04:00
Nikolaj Bjorner
4b51fe466d fix #2562 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-17 11:49:11 -04:00
Nikolaj Bjorner
69abe1687e backjump to level of clause to ensure that new atoms created by projection are assigned as assumptions fix #2557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-14 20:17:07 -04:00
Nikolaj Bjorner
0f20175bdd fix #2556, sign of of inequality is not restricted to -1, 0, 1, but can be -2, -3 etc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-14 19:41:01 -04:00
Nikolaj Bjorner
0c972b8bee tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 15:45:10 -04:00
Nikolaj Bjorner
da805f6016 address perf bottleneck exposed by #2552 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 18:31:52 +02:00
Nikolaj Bjorner
fffc539b40 fix #2549 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 17:42:29 +02:00
Nikolaj Bjorner
098725aa1c fix #2553 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 15:03:05 +02:00
Nikolaj Bjorner
67c4777514 fix #2548 fix #2530 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 15:03:04 +02:00
Andrew V. Jones
5d9ed5b0a9 Allow for __truediv__ and __rtruediv__ even when not using Python3 2019-09-13 14:23:13 +02:00
Arie Gurfinkel
1b83c677ea spacer: fixes lim_num_generalizer 
Must check that newly constructed generalization blocks
the proof obligation.

Was only checking that generalization is entailed by the transition system!
 2019-09-13 14:22:57 +02:00
Nikolaj Bjorner
63840806d8 fix #2546, retrieve model in optsmt lex before iterating 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-10 11:19:59 +02:00
Nikolaj Bjorner
0481adb87c fix #2547 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-10 06:38:27 +02:00
Arie Gurfinkel
0d3fed9a6a spacer: lemma generalizer for small numbers 
Attempts to reduce denominators in coefficients of farkas lemmas
 2019-09-09 20:32:13 +02:00
Nikolaj Bjorner
78a1f53ac9 fix #2544 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-09 18:07:03 +02:00
Nikolaj Bjorner
b1cdb3e451 add mbqi to smtfd. For Nuno, of course 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-09 11:28:25 +02:00
Nikolaj Bjorner
c22a17f430 smtfd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-08 18:14:28 +02:00
Nikolaj Bjorner
d3da161803 smtfd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-08 12:26:37 +03:00
Nikolaj Bjorner
5ba4d8d0f1 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-07 18:22:28 +03:00
Arie Gurfinkel
d44081db7d fix clang compilation errors 2019-09-07 18:21:54 +03:00
Nikolaj Bjorner
85fb6f59de disable ackermannize on goal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-07 17:56:21 +03:00