mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 22:05:36 +00:00
Code Activity
14811 commits 23 branches 48 tags 157 MiB
Commit graph

2252 commits

Author SHA1 Message Date
Nikolaj Bjorner c5432dbd88 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 09:12:09 -08:00
Nuno Lopes 3a572edb9c fix build 2021-01-20 10:42:29 +00:00
Nikolaj Bjorner 48058e706f fix #4951 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 02:21:42 -08:00
Nikolaj Bjorner 690bc51b7f fix #4927 2021-01-08 15:40:15 -08:00
Nikolaj Bjorner 60ef60dff8 euf solver updates 2021-01-07 17:32:04 -08:00
Nikolaj Bjorner 7bf691e1f9 fix bug in tracking qhead 2021-01-07 17:32:04 -08:00
Nuno Lopes 4db41c02cc remove some dead code from fpa2bv converter 2021-01-04 17:06:35 +00:00
Nikolaj Bjorner 523578e3f6 working on new solver core 2020-12-30 14:38:41 -08:00
Nuno Lopes 799de71a9f
limit recursion depth of push_not() to 8 (#4917) 2020-12-28 19:55:43 -08:00
Nikolaj Bjorner 374ae52d70 testing mbi 2020-12-26 13:49:59 -08:00
Nikolaj Bjorner 372e5ca569 fixes in new solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-25 11:19:31 -08:00
Nikolaj Bjorner 8e0a2c9e77 fix #4910 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 11:29:13 -08:00
Nikolaj Bjorner 259a8ff786 fix #4907 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 11:02:19 -08:00
Nikolaj Bjorner 7fe8298479 fix #4873 2020-12-12 16:03:48 -08:00
Nikolaj Bjorner f71204c222 fix #4879 2020-12-12 13:37:25 -08:00
Nikolaj Bjorner fae9481308 fix #4875 
remove unsound rewrite, regression
 2020-12-08 12:17:41 -08:00
Nikolaj Bjorner 97683bd48a fix #4876 2020-12-08 12:12:16 -08:00
Nikolaj Bjorner f5f980fa38 add rewrite rule 2020-12-07 21:28:23 -08:00
Nikolaj Bjorner 409414c5b3 #4655 
rewrite replace using distributivity rule.
 2020-12-07 13:12:26 -08:00
Nikolaj Bjorner 289cc9de79 add rewrites for replace_all 2020-12-07 13:02:28 -08:00
Nikolaj Bjorner 6c9bdc949e fix #4848 2020-12-07 05:59:55 -08:00
Nikolaj Bjorner 4d55f83654 misc 2020-12-04 16:59:13 -08:00
Nikolaj Bjorner bb24b3f2be fix #4836 2020-11-29 21:08:28 -08:00
Nikolaj Bjorner 17f04099a5 fix #4831 2020-11-28 11:01:07 -08:00
Nikolaj Bjorner 67a8492bd0 more graceful proof checks 2020-11-27 14:40:46 -08:00
Nikolaj Bjorner 1619311ff7 fix #4826 2020-11-27 10:42:13 -08:00
Nikolaj Bjorner d6a5ef4343 add recfuns to Java #4820 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-25 12:25:20 -08:00
Nikolaj Bjorner 291502f8e4 this-> 2020-11-22 21:20:13 -08:00
Nikolaj Bjorner 193ca57444 fix #4811 2020-11-22 16:05:44 -08:00
Nikolaj Bjorner 299e1788b8 fix #4808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-21 15:03:17 -08:00
Nikolaj Bjorner d6106f26ff disable gcd test 2020-11-20 12:18:19 -08:00
Nikolaj Bjorner ee04bfd174 fix equality propagation 2020-11-20 11:12:55 -08:00
Nikolaj Bjorner a475e7cf5a Add gcd test to bv-rewriter 2020-11-20 11:12:54 -08:00
Nikolaj Bjorner 6506d33b35 Add GCD test 2020-11-20 11:12:54 -08:00
Nikolaj Bjorner b7b7970c4a guard table erasure for representative 2020-11-20 11:12:54 -08:00
Nikolaj Bjorner 36e40a296f add logging for rewriter.flat 2020-11-16 11:20:33 -08:00
Nikolaj Bjorner 9fa17a432a bug fixes in nullability check 
@veanes @cdstanford
 2020-11-13 17:05:10 -08:00
Nikolaj Bjorner 5d10cb7af4 fix #4791 - diff is left associative 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-11 18:07:05 -08:00
Nikolaj Bjorner 7e68d546ba na 2020-11-11 17:37:07 -08:00
Nikolaj Bjorner 768e2c1d0d tune hoist-rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-09 11:25:17 -08:00
Nikolaj Bjorner 4d26aabd83 fix bug in rewriting of power 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-09 07:12:37 -08:00
Nikolaj Bjorner f78980c81c fix rewriting of power 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-08 20:58:16 -08:00
Nikolaj Bjorner 864eaf8bf8 remove unsound rewrite #4778 2020-11-08 17:48:51 -08:00
Nikolaj Bjorner e2c1436cc8 fix #4775 2020-11-08 17:18:18 -08:00
Nikolaj Bjorner 89ffb45c4f fixes to bv/dual-solver, 2020-11-08 17:18:18 -08:00
Christoph M. Wintersteiger eadf755628
Fix bonus subtraction in fp.rem. Fixes #4564. Fixes most of #2381. 2020-11-06 20:54:10 +00:00
Nikolaj Bjorner ab199dedf9 debug arith/mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-02 12:13:19 -08:00
Nikolaj Bjorner d64bc795f0 wrong assert, compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-30 10:10:59 -07:00
Nikolaj Bjorner f354671465 add parameter for scenario from #4743 2020-10-30 01:14:34 -07:00
Nikolaj Bjorner e2fbd05fe7 adding argument restriction to mbqi, fix tracking of m_src/m_dst for expr_safe_replace and avoid resetting the cache. 2020-10-27 11:41:52 -07:00