mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
13535 commits 46 branches 52 tags 178 MiB
Commit graph

13535 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
06a64669a2 heap issue of #3655 ? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:52:32 -07:00
Nikolaj Bjorner
5c2a381eb0 fix #3654 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:46:37 -07:00
Nikolaj Bjorner
9109a29a15 fix #3653 cubing could convert internal variables to external 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:42:20 -07:00
Nikolaj Bjorner
2572506efd mitigate #3657 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:34:34 -07:00
Nikolaj Bjorner
e160320e8a fix #3659 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:31:12 -07:00
Nikolaj Bjorner
b3c863fb15 fix #3660 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:05:03 -07:00
Nikolaj Bjorner
c6b4641050 fix #3649 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 10:56:27 -07:00
Lev Nachmanson
c4416f822e add an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-01 10:44:15 -07:00
Nikolaj Bjorner
65b2037ba2 add code review comments, add assertions (disabled for now) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 04:07:59 -07:00
Nikolaj Bjorner
3574a95e50 fix #3647 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 03:52:59 -07:00
Nikolaj Bjorner
f98e6a62fe fix #3648 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 03:49:48 -07:00
Nikolaj Bjorner
cc394f0fe9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 03:42:13 -07:00
Nikolaj Bjorner
d8e00bc02e fix #3644 regression introduced in #3641 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 00:26:02 -07:00
Nikolaj Bjorner
9d759a187e fix #3643 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 00:19:05 -07:00
Nikolaj Bjorner
e9bc8e2433 fix #3642 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 23:38:07 -07:00
Nikolaj Bjorner
c20b321e57 fix #3641 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 23:29:08 -07:00
Nikolaj Bjorner
d9032890e4 finish fix for #3631 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 23:03:45 -07:00
Nikolaj Bjorner
b92d8aa00e finish fix for #3631 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 22:59:31 -07:00
Nikolaj Bjorner
1d6fb6352f fix #3631 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 21:00:52 -07:00
Nikolaj Bjorner
ddc77b1100 fix #3632 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 20:53:10 -07:00
Nikolaj Bjorner
fe267803d1 fix #3634 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 20:33:42 -07:00
Nikolaj Bjorner
79183b6339 say no to local search + parallel #3636 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 20:11:25 -07:00
Lev Nachmanson
c76adfaf19 exit on success of patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-31 17:17:54 -07:00
Lev Nachmanson
086149f3f8 patch real columns when they are factors 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-31 16:50:02 -07:00
Nikolaj Bjorner
35c59e3ca0 fix #3558 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 16:47:40 -07:00
Nikolaj Bjorner
7945d42e5e fix #3613 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 15:51:10 -07:00
Nikolaj Bjorner
4ee0462beb fix #3590 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 15:43:33 -07:00
Nikolaj Bjorner
ae447cfdad fix #3603 - false positive, it is an irrational algebraic numeral 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 15:15:39 -07:00
Nikolaj Bjorner
a1f68a619d fix #3612 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 15:09:12 -07:00
Nikolaj Bjorner
7ada20c65d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 14:15:29 -07:00
Nikolaj Bjorner
6635f92842 fix #3618 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 14:10:39 -07:00
Nikolaj Bjorner
55c285c0df fix #3620 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 14:01:00 -07:00
Nikolaj Bjorner
ea6f9eb9b6 fix #3599 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 13:53:32 -07:00
Nikolaj Bjorner
e2a247a64a fix #3601 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 13:48:44 -07:00
Nikolaj Bjorner
c108b7f99c early givup #3604 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 13:46:02 -07:00
Nikolaj Bjorner
98b43322b1 collect statistics under lock #3604 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 13:33:18 -07:00
Nikolaj Bjorner
ad2e6ff2b4 fix #3607 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 12:49:48 -07:00
Nikolaj Bjorner
512aa2a9e6 fix #3609 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 12:47:03 -07:00
Nikolaj Bjorner
a51f5756ba fix #3621, the repro file is corrupted so I cannot validate the fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 12:40:24 -07:00
Nikolaj Bjorner
78626c57d5 fix #3623 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 12:36:59 -07:00
Nikolaj Bjorner
2b5247a37b fix #3625 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 12:30:13 -07:00
Nikolaj Bjorner
0ff97d5a31 fix #3626 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 11:51:52 -07:00
Nikolaj Bjorner
43e7242e35 fix #3511 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 11:14:01 -07:00
Nikolaj Bjorner
696a178c08 s 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 11:14:01 -07:00
Arie Gurfinkel
dcc8a29a05 [spacer] fix ugly bug in ground refutation generation (i.e., cex) 2020-03-31 12:39:31 -04:00
Arie Gurfinkel
2ec00cb81d Replace is_null with is_non_empty_string in spacer params 2020-03-31 11:21:05 -04:00
Arie Gurfinkel
cfe96fe92e [spacer] fixedpoint.get_answer() returns ground refutation for SAT 2020-03-31 10:13:37 -04:00
Nuno Lopes
79eb6a0e66 reduce_invertible: fix mk_diagonal for BV 0 
switch from -x to ~x
 2020-03-31 12:22:43 +01:00
Nuno Lopes
0b6b267ec4 minor code simplification in bv rewriter 2020-03-31 11:04:04 +01:00
Nuno Lopes
91497f923a reduce_invertible: recognize (* x -1) as the same as (- x) 2020-03-31 10:54:03 +01:00