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

183 commits

Author SHA1 Message Date
Lev Nachmanson da44ad7e6f added stubs for get_lower/get_upper required by theory_seq 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 13:43:23 -07:00
Nikolaj Bjorner eeba30a277 fix #1677 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 10:56:45 -07:00
Nikolaj Bjorner b4aac1ab55 revert fix to #1677 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 21:23:13 -07:00
Nikolaj Bjorner 6a0b70ee5c selective expansion of strings for canonizer to fix #1690 regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 20:42:53 -07:00
Nikolaj Bjorner 4634d1daed selective expansion of strings for canonizer to fix #1690 regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 20:37:39 -07:00
Nikolaj Bjorner c3b27903f8 fix #1677 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 11:22:01 -07:00
Nikolaj Bjorner 1e143971c3 tune for unit test, delay initialize re-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-13 11:49:33 -07:00
Nikolaj Bjorner b5f067bec5 fix #1592 #1587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-25 11:18:24 +02:00
Nikolaj Bjorner 19bb883263 fix #1581 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-23 12:12:39 +02:00
Nikolaj Bjorner 279f1986a6 fix #1575, fix #1585 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-23 07:11:15 +02:00
Nikolaj Bjorner 72f8e408fc fix #1538 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-17 11:25:07 -07:00
Nikolaj Bjorner eb1122c5cb delay updating parameters to ensure rewriting in asserted_formulas is applied using configuration overrides. Fixes build regression for tree_interpolation documentation test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-04 21:57:08 -08:00
Nikolaj Bjorner ce1b135ec3 address accessor inconsistencies between - and from #1506 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-26 14:57:17 +09:00
Nikolaj Bjorner 7b68be75c9 fixes to #1500 and #1457 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-25 13:11:20 +09:00
Bruce Mitchener 76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener 7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner 61934d8106 align semantics of re.allchar with string proposal. #1475 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 20:08:15 -08:00
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