mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
5645 commits 49 branches 53 tags 182 MiB
Commit graph

5645 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
ad16cc0ce2 fix unit test for datalog parser, fixes issue #224 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 11:16:55 -07:00
Christoph M. Wintersteiger
ac7e8b352f Improved support for UFs in FPA theory 2015-09-28 18:20:45 +01:00
Christoph M. Wintersteiger
de3ead9ff1 build fix 2015-09-28 18:20:22 +01:00
Christoph M. Wintersteiger
076e680433 Improved UF suppport in fpa2bv_converter. 2015-09-25 17:28:31 +01:00
Christoph M. Wintersteiger
2744d80642 Fixed reference counting in fpa2bv converter. 2015-09-23 14:22:02 +01:00
Christoph M. Wintersteiger
04266fccc9 Bugfix for mpf sqrt. 
Fixes #222.
 2015-09-21 20:56:07 +01:00
Christoph M. Wintersteiger
0b15fc9402 Bugfix for mpf sqrt. 
Fixes #222.
 2015-09-21 19:44:53 +01:00
Christoph M. Wintersteiger
d4b66538f9 Bug/assertion fix for power monomials in nlsat. 
Previously triggered an assertion on regressions/smt2/fp-to_real-1.smt2, but only on OSX and FreeBSD
 2015-09-17 16:31:51 +01:00
Christoph M. Wintersteiger
05d9e188f8 Reactivated smt.max_conflicts option. 
Partially fixes #216.
 2015-09-17 14:08:04 +01:00
Christoph M. Wintersteiger
f3441c6a9b tabs and indentation 2015-09-17 13:25:22 +01:00
Christoph M. Wintersteiger
d2c9b69eb3 fixed memory leak (`mem' remained allocated upon exception thrown in check_args). 2015-09-17 13:20:24 +01:00
Christoph M. Wintersteiger
2e071e89b0 tabs 2015-09-17 13:16:35 +01:00
Christoph M. Wintersteiger
4d39108808 Bugfix for fp.to_sbv 
Fixes #162
 2015-09-17 12:21:59 +01:00
Christoph M. Wintersteiger
e9565d6a7f Fixed warning message 2015-09-17 12:18:44 +01:00
Christoph M. Wintersteiger
2115ea8bb8 Bugfix for fp.sqrt. 
Fixes #220.
 2015-09-17 12:13:04 +01:00
Christoph M. Wintersteiger
52df2224e9 Disabled FP debug variables. 2015-09-16 18:04:26 +01:00
Christoph M. Wintersteiger
27f8ad288c Bugfix for fp.to_ubv. 
Fixes #162.,
 2015-09-16 14:26:53 +01:00
Christoph M. Wintersteiger
79d69cd5f0 Added FP to_ieee_bv to fpa_rewriter to enable model evaluation. 2015-09-16 12:57:05 +01:00
Christoph M. Wintersteiger
46e24e094c fixed warning message 2015-09-16 12:08:56 +01:00
Christoph M. Wintersteiger
869cd6074d Bugfix for fp.to_sbv and fp.to_ubv. 
Fixes #162.
 2015-09-15 19:03:31 +01:00
Christoph M. Wintersteiger
a1073206f9 Bugfix for FP rewriter. 2015-09-15 16:23:24 +01:00
Nikolaj Bjorner
406cd00b3a Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-15 10:54:17 +02:00
Nikolaj Bjorner
f94152c857 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-15 10:54:01 +02:00
Christoph M. Wintersteiger
d6e2fa6a60 Bugfix for MPF fma. 2015-09-14 14:07:11 +01:00
Christoph M. Wintersteiger
d0fa4e992f Bugfix for fp.to_sbv. 
Fixes #162
 2015-09-14 14:04:31 +01:00
Nikolaj Bjorner
b25e8e2288 tune lexicographic products, avoid push/pop and ensure correction sets are not used for multiple objectives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-13 16:00:45 +02:00
Guang Chen
cef7ec2157 fix implies(expr const &, expr const &) in z3++.h 2015-09-13 13:29:06 +08:00
Nikolaj Bjorner
e3840a7fc6 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-12 14:47:49 +02:00
Nikolaj Bjorner
a8b47b4fb2 enable coercions when interpolation creates MILP constraints. Issue #217 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-12 14:47:35 +02:00
Christoph M. Wintersteiger
646dcfb6e6 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-10 11:37:18 +01:00
Christoph M. Wintersteiger
25f75b60fe Bugfix for fp.mul and fp.fma for small numbers of e/s bits. 
Fixes #215.
 2015-09-10 11:37:06 +01:00
Nuno Lopes
980a0e97f8 Python 3 compat for z3.py; patch by Sarah Winkler 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-09-10 09:32:45 +01:00
Nuno Lopes
45cfb80d14 tentatively fix another issue with char signedness as reported in issue #210 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-09-10 09:01:44 +01:00
Nikolaj Bjorner
44105b7aeb reduce verbosity level of error message when equivalence checking fails 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-09 08:32:57 -07:00
Nikolaj Bjorner
d7da64f946 fix crash with incorrect bound computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-08 16:27:57 -07:00
Nikolaj Bjorner
73a8f9960f fix regressions exposed in Internal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-07 20:17:46 -07:00
Nikolaj Bjorner
d121d031e9 fix unintialized memory read exposed by nightly build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-06 14:15:08 -07:00
Nikolaj Bjorner
4be3926daa use signed character type declarations for cross platform compilation. Fixes issue #210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-05 16:30:58 -07:00
Nikolaj Bjorner
87396bd648 fix issue #212 - don't use SAT solver core when division semantics is disabled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-05 11:03:35 -07:00
Nikolaj Bjorner
09980a496c Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-02 16:12:33 -07:00
Nikolaj Bjorner
b4d0e6076e change behavior on allocation excess to process exit to avoid memory smashes on exception unsafe code blocks. Fixes issue #175 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-02 16:12:19 -07:00
Nikolaj Bjorner
1257d1d990 fix issue #196 related to resetting qe-sat tactic state over multiple calls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-01 12:36:45 -07:00
Nikolaj Bjorner
fdef17683a Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-01 10:35:34 -07:00
Nikolaj Bjorner
2bff98ca5d enable incremental bit-vector solving 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-01 09:52:48 -07:00
Christoph M. Wintersteiger
5b8d0617d4 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-01 17:52:30 +01:00
Christoph M. Wintersteiger
336fa6ae83 Bugfix for FP to BV conversion of UFs 2015-09-01 17:52:19 +01:00
Nikolaj Bjorner
cc5d719d9e enable incremental bit-vector solving 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-01 09:48:35 -07:00
Nikolaj Bjorner
963981b3a6 fix memory alias bug and non-termination bug exposed by issue #184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-31 14:45:10 -07:00
Nikolaj Bjorner
0ed38ed59b add option for using corr set and use partial cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-30 14:48:24 -07:00
Nikolaj Bjorner
7f219e84de check cancellation flag in min/max. Fixes issue #206 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-29 15:51:58 -07:00