mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-16 01:16:39 +00:00
Code Activity
13134 commits 43 branches 51 tags 169 MiB
Commit graph

791 commits

Author SHA1 Message Date
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
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
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
51e459d02b fix #3294 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 10:46:03 -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
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
Nikolaj Bjorner
c8c415c2de fix #3165 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-06 06:26:18 +01:00
Nikolaj Bjorner
8b0d540cca fix #3148 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-05 10:35:24 +01:00
Nikolaj Bjorner
67e721b5bc remove spurious false introduced when debugging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-05 09:37:03 +01:00
Nikolaj Bjorner
76d91f7d2b fix #3142 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-04 14:27:32 -08:00
Nikolaj Bjorner
a319f4bf58 fix #3104 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-02 05:16:48 -08:00
Nikolaj Bjorner
d8423a4b46 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 20:53:58 -08:00
Nikolaj Bjorner
98bd437e46 fix #3039 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 12:45:16 -08:00
Nikolaj Bjorner
8428970a1f fix #3006 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-16 23:46:58 -10:00
Nikolaj Bjorner
8c35b2092d fix #3022 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-16 08:14:51 -10:00
Nikolaj Bjorner
67cc2a8cf0 fix #2939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-05 04:51:35 -08:00
Nikolaj Bjorner
b0a28160f7 fix #2921 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-02 10:35:06 -08:00
Nikolaj Bjorner
ee62f83131 fix #2892 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-27 20:59:02 -08:00
Nikolaj Bjorner
ca11dc1fc5 remove ad-hoc rewriting of division related to comparison. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-27 17:36:02 -08:00
Nikolaj Bjorner
9c0e350bc4 rewrite3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-26 18:50:58 -08:00
Nikolaj Bjorner
c8c088e80d fix #2891 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-26 17:50:00 -08:00
Nikolaj Bjorner
e2f5c1f7c8 delay load specrels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:18:56 -08:00
Nikolaj Bjorner
f70696d8e7 reduce contention #2842 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 20:10:11 -08:00
Nikolaj Bjorner
62ea86d5d2 fix #2832 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-29 10:55:58 -08:00
Nikolaj Bjorner
1d77e3e19f fix #2830 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-26 14:41:09 -08:00
Nikolaj Bjorner
efbcdcbffd simplify diff rewriting 2019-12-20 23:20:19 -08:00
Nikolaj Bjorner
4389ed0f58 fix #2812 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-20 17:12:44 -08:00
Nikolaj Bjorner
ebb7d60c75 fix #2792 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-09 07:50:57 +03:00
Nikolaj Bjorner
99a91ee116 fix #2793 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-09 07:38:47 +03:00
Nikolaj Bjorner
7e415c1b69 update to logging 2019-12-04 23:08:41 +03:00
Nikolaj Bjorner
1eab774b91 fix #2774 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-02 15:22:03 -08:00
Nikolaj Bjorner
7e452254c3 distribute string and regex concatenation on literals, scenario exposed by #2668 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-29 11:24:18 -08:00
Nikolaj Bjorner
84025d5c11 add rewrites for moduli as exercised in example from #2319 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-24 19:02:28 -08:00
Nikolaj Bjorner
215edcf888 fix; disable rewrite. fix #2715 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-18 12:23:03 -08:00
Nikolaj Bjorner
3c6dceae7c fix #2717 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-18 12:03:59 -08:00
Nuno Lopes
b9bc6975e9 fix crash in BV internalizer due to unknown bv_neg symbol 2019-11-16 16:24:24 +00:00
Nikolaj Bjorner
a78f899225 expand deep stores by lambdas to avoid expanding select/store axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-03 10:29:10 +01:00
Nikolaj Bjorner
16d4ccd396 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-31 10:06:09 -07:00
Nikolaj Bjorner
64dd4e1c83 fix #2659 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-25 10:42:21 -07:00