Nikolaj Bjorner
|
2d0d9d462d
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2017-11-15 09:10:23 -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
|
f7e14b3283
|
add global autarky option, update translation of solvers to retain vsids, remove stale code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-14 18:19:21 -08:00 |
|
Nikolaj Bjorner
|
9ef54d7a16
|
Merge pull request #1355 from delcypher/cmake_api_doc_pass_build
[CMake] When invoking `mk_api_doc.py` pass the build directory.
|
2017-11-13 19:56:09 -08:00 |
|
Dan Liew
|
1a0bff7480
|
[CMake] When invoking mk_api_doc.py pass the build directory.
This change was requested by @wintersteiger as an alternative way
to unbreak the TravisCI builds.
|
2017-11-13 22:31:05 +00: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 |
|
Nikolaj Bjorner
|
38e4fb307c
|
add useful shorthands to Solver interface
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-13 00:00:06 -08:00 |
|
Nikolaj Bjorner
|
0f4afc4536
|
fix bug in contains function
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-12 13:45:27 -08:00 |
|
Nikolaj Bjorner
|
37b94f1f90
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-11 17:22:33 -08:00 |
|
Nikolaj Bjorner
|
6f273e7b8f
|
bug fixes in uninitialized variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-11 12:09:33 -08:00 |
|
Nikolaj Bjorner
|
d7f9a3b37d
|
fix crash bugs in sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-11 11:27:10 -08:00 |
|
Nikolaj Bjorner
|
a6da207b65
|
fix crash bugs in sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-11 11:25:43 -08:00 |
|
Christoph M. Wintersteiger
|
7c63a5cc1d
|
Fixed MSYS/MinGW build. Fixes #1335.
|
2017-11-11 16:38:53 +00:00 |
|
Christoph M. Wintersteiger
|
45975bec65
|
Improved support for MSYS/MINGW. Fixes #969.
|
2017-11-11 15:11:54 +00:00 |
|
Christoph M. Wintersteiger
|
d44d918414
|
API doc build fix. Related to #1350.
|
2017-11-11 14:19:38 +00:00 |
|
Nikolaj Bjorner
|
c522487a86
|
add iterators to C++ vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-10 16:59:35 -08:00 |
|
Nikolaj Bjorner
|
454e12fc49
|
update to vector format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-10 15:28:16 -08:00 |
|
Murphy Berzish
|
3e53d00f81
|
Merge branch 'develop' of github.com:/mtrberzi/z3 into develop
|
2017-11-09 13:33:47 -05:00 |
|
Nikolaj Bjorner
|
cb7e53aae4
|
reset backtrack level at each cube
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-09 10:04:32 -08:00 |
|
Nikolaj Bjorner
|
ee3ed3a27a
|
Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt
|
2017-11-09 09:55:41 -08:00 |
|
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 |
|