mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
14054 commits 23 branches 48 tags 157 MiB
Commit graph

357 commits

Author SHA1 Message Date
Nuno Lopes
ec1e733ef2 fix crash in qe_array ref counting due to wrong assignment operator of ptr_vector being called 
thanks to Arie Gurfinkel for reporting this
 2020-06-09 10:02:27 +01:00
Nikolaj Bjorner
57086edc42 close #4432 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 03:06:58 -07:00
Nikolaj Bjorner
9ca5b3f304 fix #4449 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 21:10:07 -07:00
Nuno Lopes
e844aef896 remove a few more copy constructors, though still not enough to enable the assertion in vector 
I give up for now; there are too many copies left for little return..
 2020-06-03 20:32:13 +01:00
Nikolaj Bjorner
3a7df2c6ef fix various nullability checks in seq_regex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 12:28:32 -07:00
Andrew V. Jones
a23ca1792b
Ensure that Z3 uses the correct SMT-LIB2 syntax for push and pop (#4495) 
* When pretty-printing SMTLIB2, ensure that Z3 uses the correct syntax for 'push'

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>

* When pretty-printing SMTLIB2, ensure that Z3 uses the correct syntax for 'pop'

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
 2020-06-03 09:35:14 -07:00
Nikolaj Bjorner
04829e6b7a fix #4437, not really interesting bug as debug assertion is really for non-interrupted flow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 18:41:26 -07:00
Nikolaj Bjorner
4ef480e2a5 add op cache 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 12:52:42 -07:00
Nikolaj Bjorner
1c2aa1076b fix #4125 2020-04-27 11:31:02 -07:00
Nikolaj Bjorner
f1193986c9 fix #4102 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-26 21:24:54 -07:00
Nikolaj Bjorner
decd69ac73 move to util 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-26 21:22:14 -07:00
Nikolaj Bjorner
6d4bd37e15 fix #4104 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-26 21:04:28 -07:00
Nikolaj Bjorner
fc1321f8b3 fix #4104 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-26 21:04:28 -07:00
Nikolaj Bjorner
c2e0491456 fix #4113 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-26 21:04:28 -07:00
Nikolaj Bjorner
a884201d62 remove using insert_if_not_there2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-25 15:08:51 -07:00
Nikolaj Bjorner
a3844af94b fix #4081 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-24 10:44:20 -07:00
Nikolaj Bjorner
25252af1fc fix #3975 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-15 08:06:43 -07:00
Nikolaj Bjorner
21a31fcd26 add missing fixed propagations on negated integer inequalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-11 02:28:38 -07:00
Nikolaj Bjorner
61fb134653 fix #3782 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-10 11:22:12 -07:00
Nikolaj Bjorner
56358a6b94 fix #3867 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 18:06:37 -07:00
Nikolaj Bjorner
dde0c9bd0d fix #3833 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 04:34:36 -07:00
Nikolaj Bjorner
16be6b9162 fix #3789 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-06 13:57:38 -07:00
Nikolaj Bjorner
bffe7a2215 fix #3783 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-06 12:19:34 -07: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
fadc3761bd fix #3731 - abuse of parameter combinations, trying to use qsat on arrays, but disabling array equality expansion during model evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 17:06:43 -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
50624723af fix #3704 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 10:38:31 -07:00
Nikolaj Bjorner
896a1b2048 fix #3679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 15:04:56 -07:00
Arie Gurfinkel
5673ec046b qe_term_graph fix for #3526 2020-03-26 16:45:06 -04:00
Nikolaj Bjorner
f158ab8395 fix #3426 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-22 20:48:31 -07:00
Nikolaj Bjorner
9f1530fdc0 fix #3428 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-22 14:34:17 -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
d1f6470805 fix #3431 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-22 13:50:33 -07:00
Nikolaj Bjorner
8717c7d7ff fix #3450, remove deprecated qe-sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-21 18:11:40 -07:00
Nikolaj Bjorner
37bc4a4407 fix #3420 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-19 17:50:23 -07:00
Nikolaj Bjorner
cd434d8bd5 fix #3420 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-19 17:49:48 -07:00
Nikolaj Bjorner
2ad1cc95c1 fix #3409 - force model completion so that variables simplified away during pre-rpocessing are evaluated nevertheless 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-19 11:17:59 -07:00
Nikolaj Bjorner
65e1d08457 disabling linearization when canceled, #3412 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-19 10:23:55 -07:00
Nikolaj Bjorner
7cb6f41d0a fix #3390 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 11:15:15 -07:00
Nikolaj Bjorner
31164c2eaf fix #3386 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 10:40:34 -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
9e41e88392 delay-initialize solver to avoid conflicts with global parameters #3076 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 11:34:49 -07:00
Nikolaj Bjorner
bed2097fc4 fix #3076 - need to apply relevancy propagation in mk_bits. Assume bv v is already relevant but did not have bits associated with it, the bits need to then be marked as relevant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 10:36:00 -07:00
Nikolaj Bjorner
170a534681 fix #3126 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-08 17:58:59 +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
c9c9efebde fix #3153 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-05 09:18:03 +01:00
Nikolaj Bjorner
67497ba897 fix #3131 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-04 09:38:36 -08:00
Nikolaj Bjorner
589db2052a fix #3064 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-21 20:26:57 -08:00
Nikolaj Bjorner
84b12dddac fix #3057 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-20 20:41:59 -08:00
Nikolaj Bjorner
ff436ecb10 fix #3038 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-19 09:52:27 -08:00