mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
7664 commits 46 branches 52 tags 178 MiB
Commit graph

7664 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
9601761a6f Added missing float conversion in fpa2bv converter. Relates to #1178. 2017-07-31 22:12:15 +01:00
Nikolaj Bjorner
8fdf3177da add initialization to unused parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 14:06:29 -07:00
Arie Gurfinkel
97c5ab30d5 small improvements to bmc engine 
courtesy of Marc Brockschmidt
 2017-07-31 17:04:36 -04:00
Arie Gurfinkel
7168451201 eager quantifier instantiation for quantified array properties 2017-07-31 17:04:16 -04:00
Arie Gurfinkel
2c7a39d580 Optionally blast arrays 
This changes the default behavior of always blasting arrays.
The old behavior can be restored using

   fixedpoint.xform.array_blast=true
 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
f5fa6b0bcb optionally disable subsumption checker 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
33c81524d2 optionally disable propagate variable equivalences in interp_tail_simplifier 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
86db446afa python spacer-specific API 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
d080c146a2 public API for spacer 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
c3d433ede0 implemented spacer-specic muz API 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
1530a39a96 stubs for spacer-specific API 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
ffa4957362 do not use array_der when simplifying rules 2017-07-31 17:02:29 -04:00
Arie Gurfinkel
a73023da97 preserve rule names when changing rules 2017-07-31 17:02:29 -04:00
Arie Gurfinkel
5b9bf74787 Spacer engine for HORN logic 
The algorithms implemented in the engine are described in the following papers

Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96

Nikolaj Bjørner, Arie Gurfinkel:
Property Directed Polyhedral Abstraction. VMCAI 2015: 263-281

Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki:
SMT-Based Model Checking for Recursive Programs. CAV 2014: 17-34
 2017-07-31 17:02:29 -04:00
Arie Gurfinkel
9f9dc5e19f increased verbosity level of smt_context 2017-07-31 17:01:47 -04:00
Arie Gurfinkel
ba6594b241 extra smt params used by spacer 2017-07-31 17:01:47 -04:00
Arie Gurfinkel
b269e6b35b comments on proof_utils 2017-07-31 17:01:47 -04:00
Nikolaj Bjorner
013127e947 fix build break based on ambiguous path resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 14:01:39 -07:00
Nikolaj Bjorner
063b6e9ea5 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 13:24:57 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Christoph M. Wintersteiger
bbf0ebcb74 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 20:18:53 +01:00
Christoph M. Wintersteiger
507356c7bf Fixed bug in fpa2bv converter. Fixes #1178. 2017-07-31 20:18:39 +01:00
Nikolaj Bjorner
d130ae2e4f Merge pull request #1181 from agurfinkel/tweaks 
Tweaks
 2017-07-31 11:55:52 -07:00
Nikolaj Bjorner
71d80ab47f fix build break based on new assertion in smt-eq-justification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 11:54:11 -07:00
Christoph M. Wintersteiger
52cf80d637 Simplified bit-vector bounds in fp.rem. Relates to #872. 2017-07-31 19:53:55 +01:00
Christoph M. Wintersteiger
ecfd241e19 Injected 3 missing bits of precision into fp.rem. Relates to #872. 2017-07-31 19:53:44 +01:00
Arie Gurfinkel
1d5713c376 move semantics for ref 2017-07-31 14:21:30 -04:00
Arie Gurfinkel
331eec8a05 option to control array_der in qe_lite 2017-07-31 14:19:16 -04:00
Arie Gurfinkel
7670b49ada mark mk_true() and mk_false() const 2017-07-31 14:14:35 -04:00
Arie Gurfinkel
15451ae858 extra flags to control quant_hoist 2017-07-31 14:13:45 -04:00
Arie Gurfinkel
be1df279ec make proof_checker less verbose 2017-07-31 14:11:07 -04:00
Nikolaj Bjorner
2ec9944edd Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 10:51:37 -07:00
Christoph M. Wintersteiger
a59907170d Fixed renormalization in fp.mul. Relates to #872. 2017-07-31 18:34:46 +01:00
Nikolaj Bjorner
3e8ce53d87 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 09:53:16 -07:00
Nikolaj Bjorner
62b8394bdd fixes #1179 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 09:52:45 -07:00
Nikolaj Bjorner
74890ca1c8 fixes #1180 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 09:37:25 -07:00
Nikolaj Bjorner
ceca9fbef0 fixes #1176 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 09:23:55 -07:00
Nikolaj Bjorner
8bd0407adf fix #1177 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 09:13:50 -07:00
Christoph M. Wintersteiger
175f042db8 Fixed renormalization in fp.fma. Relates to #872. 2017-07-28 23:01:01 +01:00
Christoph M. Wintersteiger
e677030b74 Fixed sign bug in mpf fp.fma. Relates to #872. 2017-07-28 21:39:44 +01:00
Christoph M. Wintersteiger
a30c343d7a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-28 20:24:35 +01:00
Christoph M. Wintersteiger
0610392a05 Bugfix for fp.fma. Fixes #872. 2017-07-28 20:16:13 +01:00
Nikolaj Bjorner
27114ce9dd Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-28 10:17:53 -07:00
Nikolaj Bjorner
45e31b0db3 add dummy initialization to unused variables to avoid compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 10:17:46 -07:00
Christoph M. Wintersteiger
9bbf9f618d Merge pull request #1174 from agurfinkel/build_error_fix 
fixing a build error
 2017-07-28 18:14:25 +01:00
Arie Gurfinkel
78467077f6 fixing a build error 2017-07-28 12:18:12 -04:00
Nikolaj Bjorner
31d6abcfe8 remove arity check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:55:41 -07:00
Nikolaj Bjorner
e9b9a29339 revert first fix for #1173, replace by handling single arity chainables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:44:19 -07:00
Nikolaj Bjorner
64233034cc fix #1173 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:26:52 -07:00
Christoph M. Wintersteiger
33ebdc8adc Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872. 2017-07-27 23:08:35 +01:00