mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 20:21:23 +00:00
Code Activity
13011 commits 46 branches 51 tags 172 MiB
Commit graph

1860 commits

Author SHA1 Message Date
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
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
Christoph M. Wintersteiger
6b12da0b45
Fix quasi-macro detection 2020-03-04 18:07:30 +00:00
Christoph M. Wintersteiger
19ed465696
Fix quasi-macro variable checks. Fixes #3029. 2020-03-04 16:40:36 +00:00
Nikolaj Bjorner
a319f4bf58 fix #3104 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-02 05:16:48 -08:00
Nikolaj Bjorner
1dcfe583e7 fix definition expression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 16:18:26 -08:00
Nikolaj Bjorner
15f5444b8c enable auxiliary recursive function definitions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 16:12:32 -08:00
Nikolaj Bjorner
764b991468 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 14:34:44 -08:00
Nikolaj Bjorner
3afb78416f fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 14:34:44 -08:00
Nikolaj Bjorner
5a357f9998 fixup build of example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 14:34:44 -08:00
Nikolaj Bjorner
88eb527b96 avoid const in ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 10:40:10 -08:00
Nikolaj Bjorner
a65efb682b avoid const in ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 10:40:10 -08:00
Nikolaj Bjorner
d8423a4b46 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 20:53:58 -08:00
Christoph M. Wintersteiger
963f8240c2
Throw proper warning instead of assertion violation in fp.rem. Fixes #2934. 2020-02-25 17:17:41 +00:00
Nikolaj Bjorner
dcd4fff284 fixes to cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-21 18:06:57 -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
3210dce63c fix #3038 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 12:38:25 -08:00
Nikolaj Bjorner
f810f25d8d fix #3004 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-17 19:37:47 -10:00
Nikolaj Bjorner
23a474655b fix #3034 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-17 19:09:46 -10:00
Nikolaj Bjorner
41ab578593 remove assert, remove brittle pydoc example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-17 00:35:47 -10:00
Nikolaj Bjorner
234b53b831 fix #3028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-17 00:20:01 -10: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
e9c4c23334 fix #3017 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-15 21:42:22 -10:00
Nikolaj Bjorner
17984af4cc disable automatic coersion to reals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-11 22:06:04 -08:00
Nikolaj Bjorner
67cc2a8cf0 fix #2939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-05 04:51:35 -08:00
Nikolaj Bjorner
28c827fb69 fix #2919 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-02 14:49: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
3dc822c127 fix #2903 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 18:48:27 -08:00