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

7251 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
ca67274519 another round of fix for #989 to avoid problems with doxygen generation (TravisCI build failure) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 12:59:34 -07:00
Nikolaj Bjorner
af47aa0120 updated suspenders for #989 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 12:32:44 -07:00
Nikolaj Bjorner
b902018373 add suspenders for #989 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 11:56:01 -07:00
Nikolaj Bjorner
c8b5be48de unexpressing interpolants #1172 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 11:44:52 -07:00
Nikolaj Bjorner
2e3a5a2060 attempt at addressing #989 by referencing _lib directly instead of over lib() in function calls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 11:03:18 -07:00
Nikolaj Bjorner
18e9e4f4ac fixes #1169 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 09:25:01 -07:00
Nikolaj Bjorner
21759e5eb2 fixes #1172 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 08:59:12 -07:00
Nikolaj Bjorner
6558999cef fixes #1171 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 08:46:20 -07:00
Nikolaj Bjorner
d3e1d250a7 fixes #1168 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 07:50:16 -07:00
Nikolaj Bjorner
2cc6baede5 address #1167 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 07:44:08 -07:00
Nikolaj Bjorner
1a07c6c188 address ASAN bug report #1160 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-26 20:48:49 -07:00
Nikolaj Bjorner
b1298d7bde ensure that assertions within the unit tests are exercised in all build modes, remove special handling of SASSERT for release mode #1163 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-26 20:28:55 -07:00
Nikolaj Bjorner
3f8b63f5a8 Merge branch 'master' of https://github.com/z3prover/z3 2017-07-26 19:52:11 -07:00