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

15105 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
6e14d3fbd3 fix #4795 2020-11-27 18:00:36 -08:00
Nikolaj Bjorner
df09cb7c95 fix relevancy test 2020-11-27 14:49:05 -08:00
Nikolaj Bjorner
35900ee8ea avoid crash from #4772 
To take care of "When I use options fp.xform.slice=false fp.xform.inline_eager=false Z3 actually seg-faults."
 2020-11-27 14:41:28 -08:00
Nikolaj Bjorner
67a8492bd0 more graceful proof checks 2020-11-27 14:40:46 -08:00
Nikolaj Bjorner
6771e44d93 fix #4825 #4824 2020-11-27 13:39:33 -08:00
Nikolaj Bjorner
1619311ff7 fix #4826 2020-11-27 10:42:13 -08:00
Nikolaj Bjorner
f58618aa04 fix java compile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-26 08:09:48 -08:00
Nikolaj Bjorner
b5a6c6bc66 attempt at more graceful timeout handling #4821 2020-11-26 06:33:44 -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
Murphy Berzish
6aba325cea
z3str3: reject certain unhandled expressions (#4818) 2020-11-25 12:15:35 -08:00
Nikolaj Bjorner
c27a325017 na 2020-11-23 10:22:21 -08:00
Nikolaj Bjorner
b769c0054b fix error messages for #4816 2020-11-23 10:20:52 -08:00
Nikolaj Bjorner
291502f8e4 this-> 2020-11-22 21:20:13 -08:00
Nikolaj Bjorner
1008b2d4cb fix #4812 2020-11-22 16:21:19 -08:00
Nikolaj Bjorner
193ca57444 fix #4811 2020-11-22 16:05:44 -08:00
Nikolaj Bjorner
65464f5944 include order 2020-11-22 15:39:09 -08:00
Nikolaj Bjorner
797f50e699 DRAT debugging updates 2020-11-22 15:38:57 -08:00
Nikolaj Bjorner
6d0b89a989 fix #4810 2020-11-22 15:37:55 -08:00
Nikolaj Bjorner
065e0652a3 fix crash when parsing datalog format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-21 15:15:28 -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
1b768c9b3a fix #4805 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-20 12:11:38 -08:00
Nikolaj Bjorner
1269776777 remove experimental option. Fix #4806 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-20 11:46:19 -08:00
Nikolaj Bjorner
ac1b3fc6f2 fix delay blasting and relevancy 2020-11-20 11:12:55 -08:00
Nikolaj Bjorner
9f34af5e18 update justifications only at level 0 2020-11-20 11:12:55 -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
Nuno Lopes
40159a3a96 fix single-thread build 2020-11-19 21:46:32 +00:00
John Regehr
0fa88efc2b
scoped_timer: wait for timer thread before main thread continues (#4803) 2020-11-19 21:42:55 +00:00
Nikolaj Bjorner
e16acd0965 move std::function initializer to beginning of class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-16 17:02:15 -08:00
Nikolaj Bjorner
f6f594e21d fix missing equality propagation in new bv solver 2020-11-16 16:22:56 -08:00
Nikolaj Bjorner
36e40a296f add logging for rewriter.flat 2020-11-16 11:20:33 -08:00
Nikolaj Bjorner
85a20791db fix relevancy tracking in new solver 2020-11-16 11:20:17 -08:00
Nikolaj Bjorner
36e9412252 fix #4796 2020-11-16 11:19:54 -08:00
Nikolaj Bjorner
98db260a93 relax unhandled condition 2020-11-14 14:58:43 -08:00
Nikolaj Bjorner
49a0266c6a na 2020-11-13 17:05:56 -08:00
Nikolaj Bjorner
9fa17a432a bug fixes in nullability check 
@veanes @cdstanford
 2020-11-13 17:05:10 -08:00
Nikolaj Bjorner
c15001bf69 #4532 
https://github.com/Z3Prover/z3/issues/4532#issuecomment-726867868
 2020-11-13 11:45:59 -08:00
Nikolaj Bjorner
71ac40ca23 fix #4793 2020-11-13 11:45:05 -08:00
Nikolaj Bjorner
cb4e5197fa #4740 
Fix https://github.com/Z3Prover/z3/issues/4740#issuecomment-712092917
 2020-11-12 16:55:07 -08:00
Nikolaj Bjorner
7f869e513b fix #4792 2020-11-12 13:23:34 -08:00
Nikolaj Bjorner
d61f30fdc6 force flat for solver 2, fix #4789 2020-11-12 13:01:38 -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
72e57f550d update release similar to nightly 2020-11-11 17:38:07 -08:00
Nikolaj Bjorner
7e68d546ba na 2020-11-11 17:37:07 -08:00
Nikolaj Bjorner
aced115b70 model validation 2020-11-11 17:37:07 -08:00
Nikolaj Bjorner
16db8bf49e add model validation 2020-11-11 17:37:07 -08:00
Nikolaj Bjorner
b5aab7ec2a fix clone 2020-11-11 17:37:06 -08:00