3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 03:31:23 +00:00
Commit graph

1891 commits

Author SHA1 Message Date
Lev Nachmanson
cf3f06ee26 use scoped interval
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-02 15:58:46 -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
a7aff1bcf0 fix regression on string ops
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-02 10:03:35 -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
57d430b3fd fix #3700
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-02 06:38:14 -07:00
Nikolaj Bjorner
2ac8d3461e fix #3670
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-01 15:35:53 -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
Nikolaj Bjorner
e9bc8e2433 fix #3642
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-31 23:38:07 -07:00
Nikolaj Bjorner
43e7242e35 fix #3511
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-31 11:14:01 -07:00
Nuno Lopes
0b6b267ec4 minor code simplification in bv rewriter 2020-03-31 11:04:04 +01:00
Nikolaj Bjorner
8a961a5ce9 fix #3554
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-30 15:02:55 -07:00
Nikolaj Bjorner
fe81de6d39 fix #3555
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-30 14:37:38 -07:00
Nikolaj Bjorner
9f386306ef na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-29 10:55:47 -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
d4699b181d fix assertion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-26 12:49:44 -07:00
Nikolaj Bjorner
37f080b877 fix #3523
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-26 09:44:00 -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
4dfc0d6d88 fix #3334
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
af4e1fa010 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
b41b83cd63 fix #3314
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
73d73e6c95 enhance rewriting for indexof based on #3516
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 13:29:36 -07:00
Nikolaj Bjorner
145ec8f248 pick up log configuration consistently #3513
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 10:51:55 -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
0cf401c67b fix #3458
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-23 17:27:10 -07:00
Nikolaj Bjorner
28bdda326b fix #3499
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-23 13:37:08 -07:00
Nikolaj Bjorner
bb451c39c9 fix #3495
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-23 10:32:19 -07:00
Nikolaj Bjorner
61d9960420 fix #3461
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-22 14:46:24 -07:00
Nikolaj Bjorner
70a1786061 scoping th solver to avoid memory leak during cancellation exposed by #3431
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-22 14:14:45 -07:00
Nikolaj Bjorner
d6a2e7ac15 fix #3433
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-22 13:21:48 -07:00
Nikolaj Bjorner
077024f024 fix #3435
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-22 12:14:34 -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
719c5dd911 fix #3342
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-17 12:14:28 -07:00
Nikolaj Bjorner
1c5283f3a4 remove mk_pp to fix build on some platforms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-16 20:36:41 -07:00
Nikolaj Bjorner
d002423133 fix ? #3342
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-16 20:09:28 -07:00
Nikolaj Bjorner
ed70d246d3 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-16 11:39:09 -07:00
Nikolaj Bjorner
1bddfd40c3 fix #3364
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-16 11:38:25 -07:00
Nikolaj Bjorner
a5c60ec517 Update arith_decl_plugin.cpp
use integer sorts
2020-03-15 14:30:02 -07:00
Nikolaj Bjorner
c613ab0ba0 fix #3286
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-14 11:42:26 -07:00
Nikolaj Bjorner
51e459d02b fix #3294
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-14 10:46:03 -07:00
Nikolaj Bjorner
31c3ac016a fix #3275
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-13 13:55:12 -07:00
Nikolaj Bjorner
825fbf1832 fix #3268
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-13 10:49:39 -07:00
Nikolaj Bjorner
356a9bb9ed fix #3255
The model is fine, but debug facility that checks the model reports a false positive.
It exposed some further opportunities for simplification
2020-03-12 10:57:35 -07:00
Nikolaj Bjorner
e45871d7c5 fix #3239
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-11 09:35:28 -07:00
Nikolaj Bjorner
04a19cd1d8 fix #3219
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-10 16:21:01 -07:00
Nikolaj Bjorner
a09ed766f5 fix #3226
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-10 11:41:41 -07:00
Nikolaj Bjorner
7452e55698 fix #3190 fix #3168
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-08 12:54:03 +01:00
Nikolaj Bjorner
bdd66e1fa0 fix #3180 fix #3181 #3184
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-07 12:13:43 +01:00
Nikolaj Bjorner
f501380e89 fix #3169 - set cancellation timeout and limit during push. Also expose internalization outside of scope that disables cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-06 23:36:04 +01:00