3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-26 02:01:21 +00:00
Commit graph

25 commits

Author SHA1 Message Date
Nikolaj Bjorner
0d400a5ad6 fix bit2bool bug reported by Jianying Li
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-04 07:46:53 -08:00
Nikolaj Bjorner
335d672bf1 fix #1675, regression in core processing in maxres
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-19 23:23:19 -07:00
Arie Gurfinkel
81575fae7c Remove unused function 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
0ae246ad2b add defs to arith solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:52 -07:00
Arie Gurfinkel
1e54237880 mbp_array: Fix set_model_completion bug 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
b50da20531 array_mbp: turn on model completion 2018-06-14 16:08:50 -07:00
Nikolaj Bjorner
e6401908a5 fix crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
5eacb8122d add tuple features, remove dead code from mbp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
560a26127e bind nested variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
692a701516 updates to mbp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
7642106e73 add way to unit test mbp from command line
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
20300bbf94 updates to mbqi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
bf4c35982f Debug print 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
efb1f50d00 bind nested variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
d95e167d61 updates to mbqi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
e281f85586 add way to unit test mbp from command line
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
23272f0d2f array support for mbp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
988466705c port array projection to qe_arrays
ensure it works with multi-dimensional arrays

commit on behalf of Nikolaj
2018-06-14 16:08:49 -07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
fe10f2d244 address #835
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-10 07:51:16 +01:00
Arie Gurfinkel
4e7b6b6586 proposed fix to compare 2016-03-23 19:20:57 -04:00
Arie Gurfinkel
ee125b4fe3 extend model with the value of a fresh variable 2016-03-23 19:07:50 -04:00
Nikolaj Bjorner
ec681d7565 some of Arie's fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-23 10:19:16 -07:00
Nikolaj Bjorner
c4472ce717 include more qsat features
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 12:29:23 -07:00