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 |
|
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 |
|
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
|
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
|
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 |
|
Christoph M. Wintersteiger
|
e50470f2c4
|
Added support for MSYS2
|
2017-10-30 18:24:38 +00: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
|
60b970b9ba
|
add proofs dependency to solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-28 16:23:13 -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
|
fc73271b83
|
more C fixes to model example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-25 11:20:56 -07:00 |
|
Nikolaj Bjorner
|
7ed32f4315
|
re-add model example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-25 10:48:53 -07:00 |
|
Nikolaj Bjorner
|
2c27056283
|
disable model example pending C compliance or C99 or whatever adjustment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-25 10:24:49 -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
|
7148226823
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2017-10-25 08:39:05 -07:00 |
|
Nikolaj Bjorner
|
f2ce68b899
|
Merge pull request #1324 from delcypher/c_api_construct_model_example
Add example of using Z3's new model construction C API.
|
2017-10-25 08:38:17 -07:00 |
|
Dan Liew
|
de3700e1fd
|
[CMake] Try to unbreak the C example build with older GCC versions
by forcing the language version to be C99.
|
2017-10-25 11:13:25 +01: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 |
|
Dan Liew
|
f27ac24fa0
|
Add example of using Z3's new model construction C API. This API
was requested in #1223.
This example uses the new `Z3_mk_model()`, `Z3_add_const_interp()`
, `Z3_add_func_interp()`, and `Z3_mk_as_array()` API calls.
|
2017-10-24 17:34:47 +01:00 |
|