mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
10069 commits 49 branches 53 tags 182 MiB
Commit graph

10069 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
700f413e26 updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-09 09:55:37 -08:00
Christoph M. Wintersteiger
a173b0faf7 Fixed API doc build 2017-11-09 13:34:32 +00:00
Nikolaj Bjorner
bc8681a0ea reset backtrack level after first backtrack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 22:14:59 -08:00
Nikolaj Bjorner
75b8d10f48 add backtrack level to cuber interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 21:44:21 -08:00
Christoph M. Wintersteiger
19f43713c9 Fixed Windows build of C example. 2017-11-08 21:16:03 +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
bec6c3f9e2 Fixed C example build. 2017-11-08 18:22:17 +00:00
Christoph M. Wintersteiger
a8b52419f5 Fixed C example build. 2017-11-08 18:14:42 +00:00
Christoph M. Wintersteiger
bf563bbd5f Fixed default library path order in Python API. 2017-11-08 17:29:40 +00:00
Christoph M. Wintersteiger
ef800d7b93 Fixed library path order in Python API. 2017-11-08 17:20:25 +00:00
Nikolaj Bjorner
0a9946578b use failed literal to asym branching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 09:14:21 -08: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
b099449ce1 asymm branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 07:21:49 -08:00
Nikolaj Bjorner
2746528aab fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-07 17:16:36 -08:00
Nikolaj Bjorner
16555d4886 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-11-07 11:30:09 -08:00
Nikolaj Bjorner
1a687a31b6 missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-07 11:29:51 -08:00
Nikolaj Bjorner
34c5ce7f09 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-11-07 11:28:47 -08:00
Murphy Berzish
975368e16a Merge remote-tracking branch 'upstream/master' into develop 2017-11-07 13:37:33 -05: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
Nikolaj Bjorner
303157d3b7 allow incremental mode override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 15:00:52 -08:00
Nikolaj Bjorner
6f8ff46ddb Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-11-06 10:03:03 -08:00
Nikolaj Bjorner
d97f800390 update error code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 10:02:59 -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
Nikolaj Bjorner
5813e22032 fix race condition, exception handling/throwing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 18:24:15 -08:00
Nikolaj Bjorner
9a4fb4ff76 remove ad-hoc parameters, deprecating dimacs cube mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 14:08:55 -08:00
Nikolaj Bjorner
70ee030228 updates to parallel tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 10:53:25 -08:00
Nikolaj Bjorner
e46e9cf86d work on parallel-tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-04 15:56:05 -05:00
Nikolaj Bjorner
59ea11b1a3 cube and conquer parallel tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-04 13:40:31 -05:00
Nikolaj Bjorner
6df3e47b07 disable symbol fixing in pretty printer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 09:53:47 -05:00
Nikolaj Bjorner
7c743b3d16 add direct FromFile method to solvers so that model transformations are loaded along with assertions. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 09:25:18 -05:00
Nikolaj Bjorner
ac67f97e63
Merge pull request #1338 from eactor/master 
MSYS offers a MINGW shell as well. (uses different os.uname())
 2017-11-02 06:37:52 -07:00
Nikolaj Bjorner
fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05:00
Nikolaj Bjorner
caaf0ba33c model-add/del 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-01 22:32:22 -05:00
Nikolaj Bjorner
abeaefa8fe
Merge pull request #1341 from mtrberzi/issue1274-crash 
Internalize free var before iterating eqc in theory_str
 2017-11-01 10:19:33 -07:00
Paul Ehrlich
2a459c5ff6 MSYS offers a MINGW shell as well. (uses different os.uname()) 2017-11-01 12:02:48 +01: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
3de8c193ea implementing model updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 16:11:51 -05: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
bbae5c04b2 Merge branch 'master' of https://github.com/z3prover/z3 2017-10-30 13:50:41 -05: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