mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
7813 commits 49 branches 53 tags 182 MiB
Commit graph

6348 commits

Author SHA1 Message Date
Nikolaj Bjorner
07031798ec fix occurs function used in qe_lite #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-16 01:43:35 -08:00
Nikolaj Bjorner
2e6ae8cfd2 fix crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 23:06:05 -08:00
Nikolaj Bjorner
c3364f17fa fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 21:19:22 -08:00
Nikolaj Bjorner
c3f67f3b5f fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 21:17:00 -08:00
Nikolaj Bjorner
f47671931f Merge branch 'master' of https://github.com/z3prover/z3 2017-11-15 20:32:45 -08:00
Nikolaj Bjorner
58be777307 fix #1358 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 20:32:37 -08:00
Nikolaj Bjorner
cde41cf16c fix slicer for unsoundness. #1304 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 16:39:09 -08:00
Nikolaj Bjorner
7f13cf13f2 clean up bv_numeral code and fix bug in how they are initialized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 15:00:11 -08:00
Nikolaj Bjorner
795e0c641a add method to create bit-vectors directly from an array of Booleans 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 14:44:59 -08:00
Nikolaj Bjorner
2c97eb1393 include information whether rule is reachable in del_rule model converter for simpler model presentation #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 11:46:28 -08:00
Nikolaj Bjorner
116094022f insert total relations in model converter. #1291 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 09:10:15 -08:00
Nikolaj Bjorner
195d81ebef fix rewriter loop reported in #1354 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-13 13:49:03 -08:00
Nikolaj Bjorner
dbb35b951c make .NET and Java bindings for optimization use Expr instead of ArithExpr to accomodate bit-vector optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-13 08:51:16 -08:00
Christoph M. Wintersteiger
7c63a5cc1d Fixed MSYS/MinGW build. Fixes #1335. 2017-11-11 16:38:53 +00:00
Christoph M. Wintersteiger
2d221155b3 Fixed bug in fp.to_ieee_bv with rewriter.hi_fp_unspecified=true. Reported in #1349. 2017-11-08 20:52:48 +00:00
Christoph M. Wintersteiger
17bcb37cf1 Fixed error handlers in Python API. 2017-11-08 20:09:18 +00:00
Christoph M. Wintersteiger
d2c5e0e76a Fixed problems arising from unfortunate object destruction order in the Python API. Fixes #989. 2017-11-08 16:36:47 +00:00
Nikolaj Bjorner
3350f32e1f fix #877 by bypassing exception generation during label collection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 16:00:16 -08:00
Nikolaj Bjorner
9d3518736b fix #889 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 15:25:10 -08:00
Nuno Lopes
861a0745c1 remove a few unneded mem allocations 2017-11-06 10:36:10 +00:00
Nikolaj Bjorner
0f2b1ae7c8 fix proof mode related segfaults #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 02:35:10 -08:00
Nikolaj Bjorner
16bab71df2 remove asserts for proof generation to enable mode switch in spacer virtual solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 02:18:55 -08:00
Nikolaj Bjorner
53ed1bb862 fix segfault reported as part of #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 02:05:00 -08:00
Nikolaj Bjorner
5bb5a50490 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 19:24:05 -08:00
Nikolaj Bjorner
a5efe9c29d Merge branch 'master' of https://github.com/z3prover/z3 2017-11-05 19:16:17 -08:00
Nikolaj Bjorner
429edf175f fix model converter bug in coi-filter #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 19:16:04 -08:00
Murphy Berzish
2d25355611 Merge remote-tracking branch 'upstream/master' into issue1274-crash 2017-10-31 17:07:54 -04:00
Nikolaj Bjorner
24a44a0b29
Merge pull request #1336 from mtrberzi/clean-rewriter-patch 
fix rewriter in theory_str
 2017-10-31 08:45:14 -07:00
Nikolaj Bjorner
29d643cc23
Merge pull request #1337 from mtrberzi/fix-length-testing 
Optimizations for length testing in theory_str
 2017-10-30 12:00:47 -07:00
Nikolaj Bjorner
34f24aee72 fix order of instantiation for recursive functions, #1274 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 13:50:31 -05:00
Murphy Berzish
6e31d9c3f5 internalize free var before iterating eqc in theory_str 2017-10-30 14:34:27 -04:00
Murphy Berzish
2ffffa9bed Merge remote-tracking branch 'upstream/master' into fix-length-testing 2017-10-30 14:04:10 -04:00
Murphy Berzish
a8d025f5b4 Merge remote-tracking branch 'upstream/master' into HEAD 2017-10-30 13:55:31 -04:00
Nikolaj Bjorner
9e20bfe7f9 fix virtual method override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 17:23:35 -07:00
Nikolaj Bjorner
2227db215e fix build break with virtual method override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:58:16 -07:00
Nikolaj Bjorner
b556f3ca42 fix stack overflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:41:29 -07:00
Nikolaj Bjorner
e4b595d490 add solver pool abstraction for Spacer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:10:20 -07:00
Nikolaj Bjorner
c886b6d500 fix #1330. Interpolation transformation needs to handle TRANSITIVITY_STAR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 20:53:10 -07:00
Nikolaj Bjorner
e7aa6455bc fix #1326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 19:25:25 -07:00
Nikolaj Bjorner
0589a20b46 fix #1326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 19:24:45 -07:00
Nikolaj Bjorner
0268f2243e remove ast.h reference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 09:49:53 -07:00
Nikolaj Bjorner
f5f1d019d8 missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 09:00:35 -07:00
Nikolaj Bjorner
371f0b193c move min_cut, fix #1321 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 02:59:04 -07:00
Nikolaj Bjorner
8acc924c21 ifndef/define match 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 16:34:49 -07:00
Nikolaj Bjorner
ee320fa025 fix build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 13:32:40 -07:00
Nikolaj Bjorner
31dfc0c610 fix build, fix #1322 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 13:20:19 -07:00
Nikolaj Bjorner
6300a78b82 more build errors in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 12:57:30 -07:00
Nikolaj Bjorner
48d144a6dd missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 12:51:47 -07:00
Nikolaj Bjorner
db65cc007a move more proof utils 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 10:27:48 -07:00
Nikolaj Bjorner
fc822af707 move proof utils under ast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 09:59:55 -07:00