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

5190 commits

This branch
This branch
All branches
Author SHA1 Message Date
Dan Liew b3713e7496 Refactor `mk_z3consts_java() code into mk_z3consts_java_internal()` 
and move that into ``mk_genfile_common.py``. Then adapt ``mk_util.py`` and
``mk_consts_files.py`` to call into the code at its new location.

The purpose of this change is to have Python code common to the Python
and CMake build systems separate from Python code that is only used for
the Python build system.
 2016-04-17 19:03:17 +01:00
Christoph M. Wintersteiger 14e1e247a4 Revert "nmake->make, little error" 
This reverts commit 8287f7ba82.
 2016-04-17 11:35:27 +01:00
Nikolaj Bjorner 7a317a4f07 Merge pull request #566 from xavdel/patch-1 
nmake->make, little error
 2016-04-16 17:46:04 -07:00
Xavier DELPIERRE 8287f7ba82 nmake->make, little error 2016-04-17 02:39:35 +02:00
Nikolaj Bjorner 0094b36636 fix bounds check to fix segfault reported in issue #565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 12:25:29 -07:00
Nikolaj Bjorner 1c8e0918d8 move to std::vector in replayer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 10:08:29 -07:00
Nikolaj Bjorner d383fd851a move vector<std::string to std::vector<std::string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 09:34:27 -07:00
Nikolaj Bjorner 4ebf392da7 Fixes #564: use std::vector on std::strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 09:26:13 -07:00
Nikolaj Bjorner 0f93853a4c remove labels from evaluation result 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-12 13:17:10 -07:00
Nikolaj Bjorner aa7b5d80fe extract array terms for evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-12 09:41:50 -07:00
Nikolaj Bjorner 2033719c14 fix optimization pre-processing reported by Gereon Kremer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-09 20:58:57 -07:00
Nikolaj Bjorner 6e57015a12 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-09 16:51:42 -07:00
Nikolaj Bjorner cc6f72aba7 fix handing of ite conditions that have to be included in projection, thanks to bug report by Zak 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-10 01:48:35 +02:00
Christoph M. Wintersteiger 16e487b32a Bugfix for ackermann helper 2016-04-08 17:20:09 +01:00
Christoph M. Wintersteiger bd0bd08ecf add is_considered_uninterpreted checks into acker_helper 2016-04-08 16:58:11 +01:00
Christoph M. Wintersteiger 0597b579b1 Bugfixes for bvarray2uf conversion. 2016-04-07 19:10:31 +01:00
Christoph M. Wintersteiger 5971c20653 Bugfixes for bv_trailing. 2016-04-07 13:08:17 +01:00
Christoph M. Wintersteiger 3a532c08a6 Bugfix for func_interp else-case compression 2016-04-06 19:24:08 +01:00
Christoph M. Wintersteiger e662427060 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 15:39:37 +01:00
Christoph M. Wintersteiger e527aca296 Bugfix for unspecified else-case in func_interps. 2016-04-06 15:39:32 +01:00
Nuno Lopes e2b7ad246a bv_trailing: fix compiler warning + use of ast_manager 2016-04-06 15:34:31 +01:00
Christoph M. Wintersteiger 7534b53bae Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 14:51:25 +01:00
Christoph M. Wintersteiger 86ca224460 Merge pull request #554 from MikolasJanota/trailing 
Trailing
 2016-04-06 14:25:58 +01:00
Mikolas Janota 7ad9dec6c2 Adding cpp files for bv_trailing to CMakeLists. 2016-04-06 11:04:17 +01:00
Mikolas Janota dbffc15b98 Improvements in caching of bv_trailing. 2016-04-06 11:04:15 +01:00
mikolas 9ba5bbfd33 Re-factoring and comments in bv_trailing. 2016-04-06 11:04:13 +01:00
Mikolas Janota 248feace34 fixing the behavior in bv_trailing 2016-04-06 11:04:11 +01:00
mikolas fced47386e More work on trailing 0 analysis. 2016-04-06 11:04:09 +01:00
mikolas ddb6ae4eab More work on trailing 0 analysis. 2016-04-06 11:04:07 +01:00
mikolas 78cb1e3c7b More work on trailing 0 analysis. 2016-04-06 11:04:05 +01:00
mikolas c7f1746321 Starting to work on trailing 0 analysis. 2016-04-06 11:04:03 +01:00
Nikolaj Bjorner 493b86eca7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-05 22:27:11 +02:00
Nikolaj Bjorner b97d694e5e undo model evaluation to BR_FULL pending regression in assertion violation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-05 22:26:57 +02:00
Christoph M. Wintersteiger efd923b826 Merge pull request #552 from MikolasJanota/bug_fix 
Avoiding adding spurious +0 in poly_rewriter::cancel_monomials.
 2016-04-05 19:06:19 +01:00
mikolas 05ce886afe Avoiding adding spurious +0 in poly_rewriter::cancel_monomials. 2016-04-05 17:26:48 +01:00
Nikolaj Bjorner c454b81b2c special case branching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-05 11:57:49 +02:00
Nikolaj Bjorner ed1a5797fb check that a clause was not removed to fix issue #551 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-04 20:15:49 +02:00
Nikolaj Bjorner ec5a4ba63d add documentation comment for evaluation, Issue #536 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-04 12:59:18 +02:00
Nikolaj Bjorner 9667185af0 issue #549, replace BoolVal by False, otherwise creates regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-03 12:53:50 +02:00
Nikolaj Bjorner 11e8f06272 issue #549, replace False by BoolVal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-03 12:52:15 +02:00
Nikolaj Bjorner 33e7640645 disable mb branching pending unit test analysis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-03 10:53:37 +02:00
Nikolaj Bjorner 03336ab9f2 add evaluation of array equalities to model evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-02 15:07:01 +02:00
Nikolaj Bjorner f6aaa5cc8d Merge pull request #550 from seahorn/farkas 
typo: gt -> ge
 2016-04-02 11:13:30 +02:00
Arie Gurfinkel 44d4902bb4 typo: gt -> ge 2016-04-02 10:13:14 +02:00
Christoph M. Wintersteiger ccd18283e7 Moved extension_converter func_interp entry compression to func_interp. 
Relates to #547
 2016-04-01 15:38:38 +01:00
Christoph M. Wintersteiger 3b82604590 whitespace 2016-04-01 15:37:40 +01:00
Christoph M. Wintersteiger d55a6725c9 Compressed func_interps in extension_model_converter. 
Fixes #547.
 2016-04-01 15:17:38 +01:00
Christoph M. Wintersteiger eb9c5b7cdb Disabled bogus assertions. 
Fixes #489
 2016-04-01 13:25:37 +01:00
Christoph M. Wintersteiger 852dc6d190 whitespace 2016-04-01 13:22:16 +01:00
Christoph M. Wintersteiger 405650c183 bugfix for ackr_model_converter (refcounts were off due to func_interps not being copied properly). 2016-04-01 13:17:48 +01:00