mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity
7731 commits 24 branches 48 tags 158 MiB
Commit graph

6284 commits

Author SHA1 Message Date
Nikolaj Bjorner
8b280b1f64 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-12 14:34:13 -07:00
Nikolaj Bjorner
8cf0c94e5f address some ASan leaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 14:34:04 -07:00
Nikolaj Bjorner
6ecd77d91c Merge branch 'master' of https://github.com/z3prover/z3 2017-10-12 14:17:57 -07:00
Nikolaj Bjorner
3554554533 command to exit tests early 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 14:17:52 -07:00
Nikolaj Bjorner
d338fab4f6 fix #1305 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 13:58:14 -07:00
Nikolaj Bjorner
11f1a81d7b disable failing unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 10:12:37 -07:00
Nikolaj Bjorner
6a09040a8e Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-12 07:39:38 -07:00
Nikolaj Bjorner
da2b876acb fix #1303 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 07:39:27 -07:00
Dan Liew
a3b109cc14 [ASan] Fix some leaks reported in the small object allocator 
test.
 2017-10-11 19:40:16 +01:00
Nikolaj Bjorner
c093e6d4b9 harden a few API methods against longjumps in set_error. Memory leak exposed in #1297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-11 09:53:02 -07:00
Nikolaj Bjorner
09ea370ea3 update C-example that fails to not use longjumps. Issue #1297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 12:06:19 -07:00
Nikolaj Bjorner
7f693186a0 trying to address leak reported in #1297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 07:10:04 -07:00
Nikolaj Bjorner
cae414e575 fixes for #1296, removing COMPILE_TIME_ASSERT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-09 13:59:44 -07:00
Christoph M. Wintersteiger
e0db65bb1d Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-09 19:18:46 +01:00
Christoph M. Wintersteiger
800fa3d246 Added bv_sort_ac=true to asserted_formulas::m_rewriter 2017-10-09 19:18:41 +01:00
Christoph M. Wintersteiger
5819e38606 whitespace 2017-10-09 19:17:44 +01:00
Nikolaj Bjorner
f359f23885 another fix for #1288 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 15:47:06 -07:00
Nikolaj Bjorner
d2ec927844 fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 12:34:08 +01:00
Nikolaj Bjorner
06d75a616f fix #1288, again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 11:40:17 +01:00
Nikolaj Bjorner
22fa108ffd fix #1288, again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 11:07:22 +01:00
Nikolaj Bjorner
1371caace2 fix #1287, again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 11:05:57 +01:00
Nikolaj Bjorner
52217f0600 fix #1290 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:56:05 +01:00
Nikolaj Bjorner
c72b3356c1 fix #1286 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:41:02 +01:00
Nikolaj Bjorner
6f7f957a26 likely fix for #1287 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:38:02 +01:00
Nikolaj Bjorner
a5ecf87ab8 fix #1288 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:32:38 +01:00
Nikolaj Bjorner
deba7d4d6e use idom for checking dominator relationships 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 14:35:44 +01:00
Nikolaj Bjorner
b898b07795 distinguish simplify_rec from simplify immediate argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 11:12:09 +01:00
Nikolaj Bjorner
7e4f532202 fix build by including mk_pp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 00:37:44 +01:00
Nikolaj Bjorner
76c309a595 disable caching of simplifier when applied to direct arguments of terms. Caching is only valid when applied to dominator children 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 00:20:58 +01:00
Nikolaj Bjorner
cabdc1f64c merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 00:09:28 +01:00
Nikolaj Bjorner
a18236bc7f have quantifier equality take names into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 00:07:53 +01:00
Nuno Lopes
1d12a9c86d dom_simplifier: fix dominator computation 2017-10-06 18:19:37 +01:00
Nikolaj Bjorner
31c6b3eb5b fix leak 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 16:07:25 +01:00
Nikolaj Bjorner
578b1e4684 Merge branch 'master' of https://github.com/z3prover/z3 2017-10-06 16:03:58 +01:00
Nikolaj Bjorner
c3f615dbfc reverse arguments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 16:03:43 +01:00
Nuno Lopes
9aa6386be9 fix debug build 2017-10-06 15:27:16 +01:00
Nikolaj Bjorner
e13d839e7c Merge branch 'master' of https://github.com/z3prover/z3 2017-10-06 13:43:11 +01:00
Nikolaj Bjorner
2634be01aa adding backwards pass 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 13:43:01 +01:00
Christoph M. Wintersteiger
50042ab638 removed unused variables 2017-10-06 13:00:09 +01:00
Nikolaj Bjorner
755ca46df6 adding bv_bounds tactic dominator style 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 12:15:41 +01:00
Nikolaj Bjorner
cb548404bc bail out dominators after log number of steps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 12:08:37 +01:00
Nikolaj Bjorner
6df628edc7 pin elements in expr2depth 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 11:45:29 +01:00
Nikolaj Bjorner
eac659f748 deal with empty set of post-orders 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 11:34:14 +01:00
Nikolaj Bjorner
f59cf2452d #1284 build problems 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-05 22:20:31 +01:00
Nuno Lopes
6eb442f06c Merge branch 'master' of github.com:Z3Prover/z3 2017-10-05 18:10:27 +01:00
Nuno Lopes
6268ff1fa1 dom_simplify improvements with Nikolaj 2017-10-05 18:10:20 +01:00
Christoph M. Wintersteiger
d38e15eae7 Merge pull request #1281 from levnach/dev 
add cancellation checks
 2017-10-05 16:29:46 +02:00
Nuno Lopes
110d558ee4 dom_simplify_tactic: micro opt 2017-10-05 08:53:12 +01:00
Lev Nachmanson
fd3d785a5b add this-> 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-10-04 14:49:45 -07:00
Lev Nachmanson
2828126b72 add cancellation checks 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-10-03 10:20:49 -07:00