mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity
7745 commits 23 branches 48 tags 157 MiB
Commit graph

7745 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger f5ff9fae34 Fixed bug check in bv2fpa converter. Fixes #1291. 2017-11-17 21:15:30 +00:00
Nikolaj Bjorner d380db8068
Merge pull request #1360 from levnach/dev 
avoid a warning
 2017-11-16 13:48:28 -08:00
Lev Nachmanson 62cf6aace7 avoid a warning 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-11-16 10:20:21 -08:00
Nikolaj Bjorner a68d5131c7 add bvsmod 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-16 09:00:14 -08:00
Nikolaj Bjorner 2be466f51e Merge branch 'master' of https://github.com/z3prover/z3 2017-11-16 08:55:51 -08:00
Nikolaj Bjorner 2efcd5b789 additional bit-vector operators over C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-16 08:55:40 -08:00
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 63eeb40081 Merge branch 'master' of https://github.com/z3prover/z3 2017-11-15 16:39:13 -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 61d149a724 fix java build problem with bool arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 16:18:18 -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 2cab1cccc9 Merge branch 'master' of https://github.com/z3prover/z3 2017-11-15 09:12:23 -08:00
Nikolaj Bjorner 100d9e3edb insert total relations in model converter. #1241 2017-11-15 09:12:10 -08:00
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 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
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
Christoph M. Wintersteiger a173b0faf7 Fixed API doc build 2017-11-09 13:34:32 +00: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
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