mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity
7817 commits 24 branches 48 tags 158 MiB
Commit graph

166 commits

Author SHA1 Message Date
Nikolaj Bjorner
c1c1b7378c removing axiom exposing unsoundness, replace by weaker axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 19:44:16 -08:00
Nikolaj Bjorner
f0a30ded7d add shorthand for translating models #1407 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 19:25:09 -08:00
Nikolaj Bjorner
faebbc5384 add shortcuts for concatenation and equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-08 16:17:04 +05:30
Nikolaj Bjorner
39d1ad3edb fix #1390 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-07 05:15:53 +05:30
Nikolaj Bjorner
bfe6260c58 fix #1376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 08:39:20 -08:00
Nikolaj Bjorner
7d693a5f9f fix different bug reported on #1366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 20:01:14 -08:00
Nikolaj Bjorner
841c48e04d fix break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 18:24:45 -08:00
Nikolaj Bjorner
77b74ddb88 fix #1366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 17:55:20 -08:00
Nikolaj Bjorner
d520557ad9 fix #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 11:52:15 -08:00
Nikolaj Bjorner
c5f231acdf debugging #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 08:16:41 -08:00
Nikolaj Bjorner
42fbe19814 fix #1316, segmentation fault when numeric value is not internalized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-21 18:56:36 -04:00
Nikolaj Bjorner
4d8290ebc2 update to theory_seq following examples from PJLJ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-30 14:04:02 -07:00
Nikolaj Bjorner
974eaab01c complement regular expressions when used in negated membership constraints #1224 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-28 01:38:23 -07:00
Nikolaj Bjorner
ebe9db14d5 fix regression exposed by segfault2.smt2 crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-21 14:13:43 -07:00
Nikolaj Bjorner
276fdd0e97 register auxiliary constants from projection operation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-20 08:51:24 -07:00
Nikolaj Bjorner
ead704f52f handle undefined constant cases for int.to.str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:13:10 -07:00
Nikolaj Bjorner
19bb55e396 recognize theory_i_arith to fix #1200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 10:22:36 -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
71d80ab47f fix build break based on new assertion in smt-eq-justification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 11:54:11 -07:00
Nikolaj Bjorner
62b8394bdd fixes #1179 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 09:52:45 -07:00
Nikolaj Bjorner
031d7e1b59 use iterators, update build icon for osx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 16:58:40 -07:00
Nikolaj Bjorner
08524a2d90 cleanup for warning message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 11:47:17 -07:00
Nikolaj Bjorner
be4b0ffe69 fix unsoundness bug instroduced when fixing #1125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-30 19:36:38 -07:00
Nikolaj Bjorner
c44c8284bd use worklist algorithm to avoid stack overflow #1125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-30 18:10:36 -07:00
Nikolaj Bjorner
f375016a11 disable tweak to seq until there are cycles to test further 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-19 18:23:27 -05:00
Nikolaj Bjorner
894c60bdf9 fix bug in qe-lite reported in #1086: bookkeeping of unconstrained variables only works for quantifier-free formulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-19 18:22:30 -05:00
Nikolaj Bjorner
02161f2ff7 revert internalize logic for re until debugged 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-15 21:13:25 -07:00
Nikolaj Bjorner
e67572ffa6 address issues raised in #998 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-15 20:47:59 -07:00
Nikolaj Bjorner
5be3e959ab address issues raised in #998 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-15 20:46:47 -07:00
Nikolaj Bjorner
a59ee8032c fix unsoundness bug in axiomatization of str.at. #1067 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-13 19:02:59 -07:00
Nikolaj Bjorner
79a8e9aab0 fix build break #1029 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-18 12:09:51 -07:00
Nikolaj Bjorner
3152833893 fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 18:55:47 -07:00
Nikolaj Bjorner
66e61b8a31 issues #963 #912 2017-04-17 03:06:38 -07:00
Nikolaj Bjorner
4140afa4cb add regular expression membership for range of int.to.str functions. Issue #957 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-11 10:49:42 +08:00
Nikolaj Bjorner
3a9857940e add missing axioms for str.at. Issue #953 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-25 19:31:01 +01:00
Nikolaj Bjorner
ca4ae171ea remove unsound simplification in prefix #949 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-21 07:40:35 -06:00
Nikolaj Bjorner
37ee4c95c3 adding parallel threads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 02:09:08 -08:00
Nikolaj Bjorner
7386e2f3e9 add warning for scearios of #876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:29:30 -08:00
Nikolaj Bjorner
777091e653 fix part 1 of #875 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:09:27 -08:00
Nikolaj Bjorner
c1480b4389 handle model generation from issue #748. Deal with warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-12 00:40:52 +01:00
Nikolaj Bjorner
dea3b8ddf7 address warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 13:14:36 +01:00
Nikolaj Bjorner
acba529bce fix bug in encoding of axioms for indexof. Issue #806 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 15:32:15 +01:00
Nikolaj Bjorner
e65d80dedd make semantics of extract/substr deterministic. Issue #781 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-15 18:29:51 +02:00
Nikolaj Bjorner
caf0a1e80d fix breaking change to theory-seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-05 07:22:27 +00:00
Nikolaj Bjorner
152321bce6 fix crash in poly normalizer exposed by qe. Issue #775 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-04 20:29:12 +00:00
Nikolaj Bjorner
1450594fc6 add patch to deal with bug exposed in issue #721 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 12:15:49 -07:00
Nikolaj Bjorner
2f67665c7e ensure stoi axiom even when no value is present for argument. Issue #731 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 09:40:21 -07:00
Nikolaj Bjorner
e485d1889c update replace semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-08 13:59:13 -07:00
Nikolaj Bjorner
4d9aadde35 updated consequence finder to fix bug in processing enumeration types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-31 16:15:36 +08:00
Nikolaj Bjorner
879f792125 fix axiomatization of str.replace. Fixes issue #703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 06:13:52 -07:00