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

3251 commits

Author SHA1 Message Date
Nikolaj Bjorner d94e12104d Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-07-30 11:32:29 -03:00
Nikolaj Bjorner a0894ac7bf add basic example of using optimizaiton context to Java as raised in issue #179 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-30 11:32:14 -03:00
Christoph M. Wintersteiger 9d31b64273 Enforced well_sorted_check/type_check by default (to match default parameter settings and to produce better error messages). 
Fixes #180

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-07-30 09:32:14 +01:00
Christoph M. Wintersteiger 0cd406ca0b Fixed initialization order and unused variable warnings. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-07-30 09:09:13 +01:00
Christoph M. Wintersteiger 7c282d3719 bugfix for smt::model_finder::set_cancel 
follow-up to fixed #178
 2015-07-29 17:18:15 +01:00
Christoph M. Wintersteiger b9e273800c Made quantifier-related parts of smt::model_finder and smt::model_checker interruptable. 
Fixes #178
 2015-07-29 16:55:45 +01:00
Nikolaj Bjorner 0e886cfe5e add default constructor and tester to python API, fixes issue #168 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-28 22:54:37 -03:00
Nikolaj Bjorner 318ee3a86d fix issue #176 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-28 22:31:41 -03:00
Ken McMillan 52de96fcfc merge with unstable 2015-07-27 11:24:17 -07:00
Ken McMillan 5aa74644fc fix for issue #171 (interpolation crash) 2015-07-27 11:15:33 -07:00
Nikolaj Bjorner fc3e1af4a9 add dump_models option per suggestion from Pankaj Chauhan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-24 09:45:17 -07:00
Henning Guenther 5fdc104f82 Improve filter_rules performance 
Perform lookup and insert in one operation to avoid duplicate work.
 2015-07-23 16:08:09 +01:00
Nikolaj Bjorner 5718c23632 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-07-16 18:01:16 -07:00
Nikolaj Bjorner 7d5c144dfe add java Optimize context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-16 18:00:45 -07:00
Nikolaj Bjorner 92f731e51c add java Optimize context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-16 18:00:26 -07:00
Nuno Lopes f62a192357 remove __in/__out SAL annotations. 
They break the build with recent glibc versions and apparently noone is using them.

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-07-15 13:46:32 +01:00
Nikolaj Bjorner d7b3aaffbd Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-07-14 13:18:16 -07:00
Christoph M. Wintersteiger 1bad614646 Fixed .equals for AST, FuncDecl, and Sort, and AST.compareTo in Java 
Fixes #143
 2015-07-14 13:09:00 -07:00
Christoph M. Wintersteiger 5f755a5bd8 Adjusted return types of set functions to ArrayExprs in Java and .NET 
Fixes #137
 2015-07-14 13:07:16 -07:00
Christoph M. Wintersteiger 31eb738db5 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-07-14 12:08:34 -07:00
Christoph M. Wintersteiger f9e2ad76fa Bugfix for fp.to_sbv 
Fixes #114.
 2015-07-14 12:05:45 -07:00
Nikolaj Bjorner 6e22250d1a fixup model construction on undef results for arithmetic. Fixes issue #161 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-13 12:44:55 -07:00
Nikolaj Bjorner 96c8b1e7ff fixup model construction on undef results for arithmetic. Fixes issue #161 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-13 12:44:07 -07:00
Nikolaj Bjorner e13bf2424e fix type checking for non-associative basic operations, fixes issue #160 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-13 08:29:24 -07:00
Nikolaj Bjorner 6fbc8fa06c break stack abuse in relevancy propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-12 14:52:43 -07:00
Nikolaj Bjorner 21201371ed add reference equality to Symbols for .NET 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-11 00:53:13 -07:00
Ken McMillan e6516f549d fail gracefully on interpolation errors 2015-07-10 14:39:11 -07:00
Ken McMillan 1cf24f7cdc issue #48 disabled rounding for strict real inequalities 2015-07-10 11:00:13 -07:00
Nikolaj Bjorner ade9b2830a various partial fixes for issue #143 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-10 08:16:57 -07:00
Nikolaj Bjorner a9a5a69b73 remove double underscores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-09 13:31:22 -07:00
Nikolaj Bjorner 4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Nikolaj Bjorner f145ceecb4 remove default failure on proof mode fixes #121 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 22:12:41 -07:00
Nuno Lopes 5703abd3f1 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-07-08 13:39:26 +01:00
Nuno Lopes 8edd551f20 remove uneeded calls to datalog_context::get_rules(), since it can be expensive. 
thanks to Henning Guenther for finding this.

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-07-08 13:39:15 +01:00
Nikolaj Bjorner 57c51493ef Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-07-07 16:01:57 -07:00
Nikolaj Bjorner d815cf9b7b fix bug in optimization where a variable is updated twice 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-07 16:01:48 -07:00
Nikolaj Bjorner e2adcc19ec fix unit test for default exception 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-06 22:52:44 -07:00
Nikolaj Bjorner 940fed16e1 enforce stringstream formatting to avoid default format routine. fixes issue #149 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-06 09:11:52 -07:00
Nikolaj Bjorner 3fd5d0eaba handle variables and quantifiers, fixes issue #150 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-06 08:34:54 -07:00
Nuno Lopes eeef4d29d6 remove the optimization for 0-byte allocations 
I wasn't able to trigger with any SMT or API benchmark
Removing it ensures the function never returns null and enables further optimizations.
I get an amazing avg speedup of 0.9%

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-07-01 14:38:33 +01:00
Nuno Lopes 1f619fd960 cleanup warnings from new dataflow engine 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-30 08:47:37 +01:00
Nikolaj Bjorner 769127d531 add dummy file to fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-29 15:10:38 -07:00
Henning Guenther c7e96d897a Replace cone-of-influence filter with generalized dataflow-engine 
Signed-off-by: Henning Guenther <t-hennig@microsoft.com>
 2015-06-29 10:50:51 +01:00
Nuno Lopes 3104d2954c don't crash in Z3_model_eval API if not given a valid expression 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-26 18:33:13 +01:00
Nikolaj Bjorner e81dc5a0a0 fixes issue #143 and memory leak on theory plugin setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-26 09:03:56 +02:00
Nuno Lopes f29d82858f make check_relation::check_equiv() exit only when solver return SAT (ie, avoid false-positives with unknowns) 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-24 17:13:24 +01:00
Nuno Lopes 30eb461e01 disable debug output from check_relation 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-24 17:06:22 +01:00
Nuno Lopes 5cc8c8bde6 udoc: micro optimization for compiler_guard 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-24 17:06:21 +01:00
Nikolaj Bjorner 6bf87083ef fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:20 +01:00
Nikolaj Bjorner 1544105bd5 set undo trail after set-watches to avoid crash during exception handling (the relevancy trail is scoped so ends up traversing the trail if allocating the watch throws an exception). Fixes crash.smt in issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:20 +01:00
Nikolaj Bjorner 03034e7b33 disable bottom-up COI on rules with negated predicates. Fixes issue #140 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:19 +01:00
Nikolaj Bjorner cd05edf833 add model on unknown, to address issue #139 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:18 +01:00
Nikolaj Bjorner 3de2a70a48 move functionality from qe_util to ast_util 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:17 +01:00
Nikolaj Bjorner 7b918e83c3 fix distribute forall, fixes issue #138 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:16 +01:00
Nikolaj Bjorner 020620aadd disable qf-ufnra tactic from default for testing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:16 +01:00
Nikolaj Bjorner 8df919b6bb fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:15 +01:00
Nikolaj Bjorner aa4b9e68d7 exposing facility to extract dependent clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:14 +01:00
Nikolaj Bjorner 38113e8434 include statistics from sub-modules for QF_UFNRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:13 +01:00
Nikolaj Bjorner 238e38eaa2 update unit tests for num allocs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:12 +01:00
Nikolaj Bjorner 158a5dd2db add count of memory allocations and way to limit allocations globally. Fix purification in nlsat_smt to fix regressions on QF_UFNRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:12 +01:00
Nikolaj Bjorner e7385d60fb fixes to githup issue #133 and stackoverflow reported bug on assertion violation in poly_simplifier_plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:11 +01:00
Nikolaj Bjorner 45d2ffa38c hide new behavior until tested 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:10 +01:00
Nikolaj Bjorner 5aee077d55 enable incremental sat for QF_BV 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:10 +01:00
Nikolaj Bjorner 0518e69d2a isolate inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:09 +01:00
Nikolaj Bjorner 22c0a593e7 deal with unit test failure cases, fixes #132 #133 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:08 +01:00
Nikolaj Bjorner 1bdedec920 add missing copyright 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:08 +01:00
Nikolaj Bjorner baf95ce4e8 add missing copyright 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:07 +01:00
Matthias Schlaipfer 37cb5b9597 Fixed a bug in udoc_relation's join project 
An optimization was applied in too many cases and led to wrong results.

Signed-off-by: Matthias Schlaipfer <t-matsch@microsoft.com>
 2015-06-24 17:06:06 +01:00
Nikolaj Bjorner 8fc6789955 remove spurious print statement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:06 +01:00
Nikolaj Bjorner 1a5327e427 strengthen quantifier check for PDR (and other engines) that don't handle quantified predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:05 +01:00
Christoph M. Wintersteiger 9a62d989e6 Revert "Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable" 
This reverts commit d3db21ccde, reversing
changes made to e463d5d899.
 2015-06-24 17:06:04 +01:00
Christoph M. Wintersteiger 3a49223076 Merge branch 'unstable' of https://github.com/wintersteiger/z3 into unstable 2015-06-14 19:00:09 -07:00
Christoph M. Wintersteiger 0caf3bd18c Bugfix for mpf.is_regular 2015-06-14 18:59:46 -07:00
Aleksandar Zeljic 66e585e817 Merge branch 'unstable' of https://github.com/AleksandarZeljic/z3 into smallFloats 2015-06-12 18:35:59 +02:00
Aleksandar Zeljic 421b3af8bd Minor additions and cleanup to the outdated code. 2015-06-12 18:35:32 +02:00
Christoph M. Wintersteiger 28fce367b1 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-12 13:00:06 +01:00
Christoph M. Wintersteiger 6980fb3035 Bugfix for distinct of floats. 2015-06-12 12:58:19 +01:00
Christoph M. Wintersteiger f84d6bf5bb Bugfix for QF_FP tactic 2015-06-12 12:58:07 +01:00
Aleksandar Zeljic f45fcbe282 Added support for patching of models containing toIntegral, max, min. 2015-06-12 11:47:58 +02:00
Nikolaj Bjorner ca31c979fe re-enable transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-11 12:00:21 -07:00
Nikolaj Bjorner 868b430b8b use scoped pointers instead of explicit deallocation (robust under exceptions) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-11 10:19:29 -07:00
Nikolaj Bjorner 94f8ecb06d Merge pull request #126 from ahorn/minimum 
Basic infrastructure for minimum aggregation function
 2015-06-11 09:38:39 -07:00
Christoph M. Wintersteiger 2c2a77174c Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-11 16:57:46 +01:00
Christoph M. Wintersteiger 31cb81111d Bugfix for fp.roundToIntegral 2015-06-11 16:56:36 +01:00
Alex Horn 4a2eef132d Merge branch 'unstable' of https://github.com/Z3Prover/z3 into minimum 2015-06-11 16:28:44 +01:00
Alex Horn 8c097044e8 Add basic compiler support for min aggregation function 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-11 16:23:26 +01:00
Alex Horn c8a123b7dd Disable a few rule transformations 
For this prototype, we need to disable three rule transformations,
namely coi_filter, similarity_compressor, rule_inliner. But
disabling the inliner causes problems with the tracer in the
datalog interpreter. Since a new proprocessor is underway, we
skip the problematic trace outputs for now.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-11 16:16:47 +01:00
Christoph M. Wintersteiger d3df473279 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-11 12:53:31 +01:00
Christoph M. Wintersteiger 5bd55420a4 C API parameter annotation fix 2015-06-11 12:53:22 +01:00
Alex Horn 565c0f785f Fix memory leaks 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-11 09:20:52 +01:00
Alex Horn bd57994f78 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into minimum 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>

Conflicts:
	src/test/dl_table.cpp
 2015-06-10 20:35:28 +01:00
Alex Horn 132f984d51 Add syntactical min checker 
The purpose of this patch is to find out more about the "shape" of
the constraints in our benchmarks. In particular, we would like to
determine whether aggregation and negation, together, appear in
recursive rules.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 20:19:14 +01:00
Alex Horn 9b7c5658c8 Ignore min aggregation functions in compiler for now 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 20:06:09 +01:00
Alex Horn e6ffa5d2a5 Enable datalog plugin for AST extensions 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 19:59:57 +01:00
Nikolaj Bjorner d469a16bb8 add more Copyright notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:59:21 -07:00
Nikolaj Bjorner b08ccc7816 added missing Copyright forms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:54:02 -07:00
Aleksandar Zeljic 08b3f9b46e Removed the fpa2bv_porec model converter which was outdated and causing evaluation bugs. 2015-06-10 19:57:32 +02:00
Alex Horn 140fb7942d Add datalog infrastructure for min aggregation function 
This patch adds an instruction to the datalog interpreter and
constructs a new AST node for min aggregation functions.

The compiler is currently still work in progress and depends on
changes made to the handling of simple joins and the preprocessor.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 18:14:14 +01:00
Christoph M. Wintersteiger 004bf1471f Added conversion function for Goal to Expr conversion in .NET, Java, ML 2015-06-10 13:17:34 +01:00
Aleksandar Zeljic a37ec41370 Buggy version, a full model is found but evaluation finds it to be invalid. 2015-06-09 21:16:53 +02:00
Christoph M. Wintersteiger 98f2de3216 Added Z3_fpa_get_numeral_significand_uint64 to .NET, Java, and ML APIs. 2015-06-09 12:57:19 +01:00
Christoph M. Wintersteiger da3243fb07 FPA API bugfix 2015-06-09 12:29:05 +01:00
Christoph M. Wintersteiger eb3d499888 documentation fix 2015-06-09 12:28:52 +01:00
Christoph M. Wintersteiger d39969f0a0 Added extraction of uint64 significand bits from FP numerals. 2015-06-09 12:28:23 +01:00
Christoph M. Wintersteiger 624cc8a874 Bugfixes for FPA API. Thanks to Christian Dernehl for reporting these. 2015-06-09 11:53:43 +01:00
Christoph M. Wintersteiger f920644892 Parameter fix for the qflia default tactic 2015-06-08 15:37:17 +01:00
Christoph M. Wintersteiger 24a5ff825a Fixed collect_param_descrs in pb2bv tactic. 2015-06-08 15:36:00 +01:00
Christoph M. Wintersteiger 3e1042c680 Exported the quasi-pb probe as per user request. 2015-06-08 15:35:29 +01:00
Nuno Lopes 0997d0d2b5 add new C API function: Z3_finalize_memory() 
Useful to debug memory leaks in Z3 and in client applications

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-07 14:55:15 +01:00
aleze648 444dc0ed0a Added missing cases for positive zero, negative zero and is positive. 2015-06-07 05:31:10 -07:00
Nuno Lopes 6217804ed5 fix another UB in bit_vector 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-07 12:07:24 +01:00
Nuno Lopes 2733899c01 remove unused var 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-05 09:30:44 +01:00
Nuno Lopes b65d5797f8 optimize expr_safe_replace for when a subexpression has no substitutions 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-03 17:21:01 +01:00
Nikolaj Bjorner 9734407cde disable throttle on unbounded objectives in shared theories. It may violate an interface equality, to fix issue #120 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 11:14:59 -07:00
Christoph M. Wintersteiger 5c67db8dc6 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 19:00:15 +01:00
Nikolaj Bjorner 171ef5c8e3 Merge pull request #117 from mschlaipfer/unstable 
Missing input format option "-dl" and non-deterministic behaviour in fixpoint engine
 2015-06-02 10:48:17 -07:00
Nikolaj Bjorner c09ac5422b fix by anomaly detection, issue #118 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 10:42:03 -07:00
Christoph M. Wintersteiger bee22a306e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 18:41:28 +01:00
Christoph M. Wintersteiger c910ed2eae fpa2bv_approx: bugfix for fp.abs 2015-06-02 18:40:11 +01:00
Nikolaj Bjorner bb210d225a Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-02 10:38:50 -07:00
Nikolaj Bjorner d06207f072 remove ite terms from objectives to synchronize values in tableau with objective value. Fixes part of (three repros) from issue #120 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 10:38:22 -07:00
Christoph M. Wintersteiger a93bb92240 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 18:36:45 +01:00
Christoph M. Wintersteiger 81218c0983 Bugfix for fp.fma 2015-06-02 18:36:19 +01:00
Christoph M. Wintersteiger f68469173f Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 18:32:01 +01:00
Christoph M. Wintersteiger 3f32732ec9 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-02 18:31:31 +01:00
Christoph M. Wintersteiger a7b12e6321 Bugfix for fp.fma with sbits <= 3 2015-06-02 18:31:09 +01:00
Christoph M. Wintersteiger 610c549104 fpa2bv_approx: added fp.abs, fixed rounding mode model extraction 2015-06-02 18:17:49 +01:00
Christoph M. Wintersteiger 65a6845945 Bugfix for fpa2bv_converter_prec 2015-06-02 17:19:31 +01:00
Christoph M. Wintersteiger 599e5b6838 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 17:16:42 +01:00
Nikolaj Bjorner ffff006945 remove old files 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 09:15:08 -07:00
Christoph M. Wintersteiger a07cba72bc eliminated unused variables 2015-06-02 17:15:07 +01:00
Christoph M. Wintersteiger 8f388d83a2 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-02 17:00:44 +01:00
Nikolaj Bjorner 7161d6c150 fixes crash from issue #119 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 08:48:37 -07:00
Matthias Schlaipfer bc94007207 Fixed non-deterministic behaviour in relation_map 
Use of ptr_hash and subsequent iteration led to non-deterministic behaviour in Datalog engine.

Signed-off-by: Matthias Schlaipfer <t-matsch@microsoft.com>
 2015-06-02 14:58:31 +01:00
Christoph M. Wintersteiger 17c06199a8 Relaxed BV type checking, follow up to issue #116 2015-06-02 12:46:30 +01:00
Christoph M. Wintersteiger c7fd74e8ad Fixed FPA Python doctest 2015-06-02 12:45:55 +01:00
Christoph M. Wintersteiger d6398c4fdc Fixed FPA Python doctest 2015-06-02 11:59:55 +01:00
Matthias Schlaipfer aee1813056 Added missing input format option "-dl" 
Signed-off-by: Matthias Schlaipfer <t-matsch@microsoft.com>
 2015-06-02 09:49:08 +01:00
Nikolaj Bjorner d4dd608bad improve type checking and reporting, fixes issue #116 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-01 14:11:31 -07:00
Nikolaj Bjorner 46a5aeaef1 improve type checking and reporting, fixes issue #116 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-01 14:10:22 -07:00
Nikolaj Bjorner 168ea2e948 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-01 09:22:27 -07:00
Nikolaj Bjorner 6f42cbd325 remove std-out 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-01 09:22:19 -07:00
Christoph M. Wintersteiger 8d55159dc8 Proper declaration of locals to make clang happy. 2015-05-30 15:23:30 +01:00
Christoph M. Wintersteiger 5ae2dd9c74 Bugfix for QF_FP default tactic. 2015-05-30 15:20:07 +01:00
Christoph M. Wintersteiger fde873ac09 Bugfix for rounding in FP to_sbv. 
Fixes #113
 2015-05-30 14:50:15 +01:00
Christoph M. Wintersteiger d47832d69c Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-30 12:12:37 +01:00
Christoph M. Wintersteiger e240e6c430 Bugfix for variable renamings (fec815b41e) 2015-05-30 12:12:23 +01:00
Nikolaj Bjorner 2d409c6042 revert bug introduced to avoid stack overflow in arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-29 14:32:24 -07:00
Nikolaj Bjorner 894d6cb11b fix build break to support new statistics items 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-29 13:38:54 -07:00
Nikolaj Bjorner f8e2fa0337 fixes issue #93 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-29 11:11:13 -07:00