mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity
8115 commits 23 branches 48 tags 157 MiB
Commit graph

8115 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 4520fafa8c fix #1368 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-26 19:13:35 -08:00
Nikolaj Bjorner 7d693a5f9f fix different bug reported on #1366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 20:01:14 -08:00
Nikolaj Bjorner 841c48e04d fix break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 18:24:45 -08:00
Nikolaj Bjorner 77b74ddb88 fix #1366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 17:55:20 -08:00
Nikolaj Bjorner 1c5f798cbe expose extra symbols for logic ALL, requested in #1364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 12:03:47 -08:00
Nikolaj Bjorner 441c0de3c8 Merge branch 'master' of https://github.com/z3prover/z3 2017-11-23 11:17:58 -08:00
Nikolaj Bjorner 357b4b20fd fix #1365. Filter MBQI instantiations for as-array terms that lead the array theory to return unknown and therefore block further instantiations. as-array terms are at this point almost always created from internal model values so quantifier instantiations with these have little value, other than instantiations of other paraameters that may indepdendently help 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-23 11:17:41 -08:00
Nikolaj Bjorner 56cc0a9018 remove redundant argument #1364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 15:47:27 -08:00
Nikolaj Bjorner 2597ac6756 fix argument validation to new overflow/underflow functions #1364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 15:44:15 -08:00
Nikolaj Bjorner 18200f55ed add bit-vector over/underflow checks to Python API, #1364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 15:14:49 -08:00
Nikolaj Bjorner d520557ad9 fix #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 11:52:15 -08:00
Nikolaj Bjorner c5f231acdf debugging #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 08:16:41 -08:00
Nikolaj Bjorner 33e8113c9e adding instrumentation to debug #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-20 16:51:17 -08:00
Nikolaj Bjorner 14714f2803 Merge branch 'master' of https://github.com/z3prover/z3 2017-11-19 20:42:11 -08:00
Nikolaj Bjorner 620bd81269 avoid rationals for addition in checked_int64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-19 20:41:42 -08:00
Christoph M. Wintersteiger 0194df611c Merge branch 'master' of https://github.com/Z3Prover/z3 2017-11-17 21:15:36 +00:00
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
Murphy Berzish 3e53d00f81 Merge branch 'develop' of github.com:/mtrberzi/z3 into develop 2017-11-09 13:33:47 -05: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