3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-14 16:36:39 +00:00
Commit graph

1176 commits

Author SHA1 Message Date
Nikolaj Bjorner
5e0c34cae2 fix #3953
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-14 09:43:03 -07:00
Nikolaj Bjorner
f564c325d3 fix #3957
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-14 06:46:10 -07:00
Nikolaj Bjorner
299a6f4aee fix #3939
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-13 14:00:21 -07:00
Nikolaj Bjorner
db9d6d12fc fix #3836 remove unused and buggy hoist_cmul
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-11 15:27:18 -07:00
Nikolaj Bjorner
dea922ba25 fix #3909
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-11 13:56:07 -07:00
Nikolaj Bjorner
6ca039c855 fix #3919
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-11 12:31:38 -07:00
Nikolaj Bjorner
addbe55823 fix #3846, another bug in eq2bv-tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 19:55:40 -07:00
Nikolaj Bjorner
dde0c9bd0d fix #3833
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-08 04:34:36 -07:00
Nuno Lopes
3313590b95 fix #3713: too much caching in dom-simplify for OR expressions 2020-04-06 12:11:26 +01:00
Nikolaj Bjorner
b889b110ee bool_vector, some spacer tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-05 12:59:04 -07:00
Nikolaj Bjorner
39ffc4ece7 fix #3759
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-05 11:19:23 -07:00
Nikolaj Bjorner
eacde16b3e fix #3199
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-04 23:55:44 -07:00
Nikolaj Bjorner
e419565239 fix #3751
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-04 23:01:30 -07:00
Nikolaj Bjorner
8faf35e2e0 fix #3735
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-04 16:47:00 -07:00
Nikolaj Bjorner
9fbe178de4 fix #3735
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-04 16:36:54 -07:00
Nikolaj Bjorner
c70e9af09d fix #3734
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-04 12:53:24 -07:00
Nikolaj Bjorner
6f65051f2c silence some build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-03 17:11:34 -07:00
Nikolaj Bjorner
426e4cc75c fix #3557
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-03 16:37:59 -07:00
Nikolaj Bjorner
918b6a8c03 trace & threads = undef
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-03 13:58:22 -07:00
Nikolaj Bjorner
cd2f6705aa fix #3715
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-03 12:05:48 -07:00
Nikolaj Bjorner
8e033c1e71 fix #3716 fix #3719
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-03 12:05:48 -07:00
Nikolaj Bjorner
896a1b2048 fix #3679
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-02 15:04:56 -07:00
Nikolaj Bjorner
f98b94bdbc fix #3680
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-02 15:04:56 -07:00
Nikolaj Bjorner
2d01c64d2c fix #3682
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-02 12:30:25 -07:00
Nikolaj Bjorner
3eefd18c58 fix #3688
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-02 09:59:16 -07:00
Nikolaj Bjorner
4f22e8c698 fix #3663
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-01 11:57:07 -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
c6b4641050 fix #3649
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-01 10:56:27 -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
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
91497f923a reduce_invertible: recognize (* x -1) as the same as (- x) 2020-03-31 10:54:03 +01:00
Nikolaj Bjorner
f21b60a6e1 remove output from normalize bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-30 17:46:53 -07:00
Nikolaj Bjorner
296e56c28f fix #3575
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-30 17:26:43 -07:00
Nikolaj Bjorner
330b3cc8d6 fix #3584
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-30 16:50:53 -07:00
Nikolaj Bjorner
b9dd18483c fix #3571
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-30 14:11:36 -07:00
Nikolaj Bjorner
de2ad26826 fix #3568
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-30 13:51:45 -07:00
Nikolaj Bjorner
1a995da0ae fix #3538, turn on proof checking assertions in goal.cpp for earlier coverage
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-29 10:55:47 -07:00
Nikolaj Bjorner
f8dcaa8885 'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-27 10:23:00 -07:00
Nikolaj Bjorner
5da2169a0e fix #3524
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-26 10:38:13 -07:00
Nikolaj Bjorner
c165f69248 fix #3525
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-26 09:44:00 -07:00
Nikolaj Bjorner
ea396a008a fix #3504
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 02:30:51 -07:00
Nikolaj Bjorner
0609408fd7 fix #3510
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 01:50:30 -07:00
Nikolaj Bjorner
519c0d5f11 fix #3434
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-23 11:51:21 -07:00
Nikolaj Bjorner
84090aaf24 fix #3423
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-23 10:27:42 -07:00
Nikolaj Bjorner
9366311844 fix #3464
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-22 14:28:56 -07:00
Nikolaj Bjorner
6c1d0f6ea0 fix #3438
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-22 11:27:20 -07:00
Nikolaj Bjorner
67fc369df0 fix #3467
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-22 11:16:06 -07:00
Nikolaj Bjorner
fcd1f2b3cd fix #3459
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-21 18:11:40 -07:00