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

4047 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner f3b8fe130a adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities. This is to address issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:40:54 -07:00
Nikolaj Bjorner 9b3e242990 adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:37:59 -07:00
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