3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-24 13:18:55 +00:00
z3/src
Nikolaj Bjorner ea201a776d enable qsat-opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-11 10:39:27 -07:00
..
ackermannization Adding translation to ackr_model_converter. 2016-06-06 18:06:45 +01:00
api Added __nonzero__ and __bool__ functions to Python Z3 ASTs to enable use of Python lists (and similar). 2016-06-08 12:07:13 +01:00
ast Bugfix for fp.min/fp.max in fpa2bv converter; hide BV UFs from FP models. 2016-06-09 17:51:31 +01:00
cmd_context test variants for seq_solver 2016-05-30 18:15:10 -07:00
duality fix warnings for unused variables 2016-05-17 13:54:22 -07:00
interp fix unused-but-set-variable warnings reported in #579 2016-05-18 11:02:10 -07:00
math Take into account number of monomials for rlimit counting 2016-06-08 11:17:26 +09:00
model avoid use-before-def crashes fp-operations.smt2 2016-05-25 14:32:39 -07:00
muz Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-08 13:56:12 -07:00
nlsat fix warnings for unused variables 2016-05-17 13:54:22 -07:00
opt enable qsat-opt 2016-06-11 10:39:27 -07:00
parsers fix warnings for unused variables 2016-05-17 13:54:22 -07:00
qe reduce warnings 2016-05-23 14:32:51 -07:00
sat fix unused-but-set-variable warnings reported in #579 2016-05-18 11:02:10 -07:00
shell add support to build with MSVC /Gr (fastcall mode for x86) 2016-03-24 15:39:18 +00:00
smt fix memory leak Issue #643 2016-06-09 21:59:10 -07:00
solver fixes to #596 and #592: use exponential step increments on integer problems, align int.to.str with canonizer and disequality checker 2016-05-17 01:00:42 -07:00
tactic Bugfix for fp.min/fp.max in fpa2bv converter; hide BV UFs from FP models. 2016-06-09 17:51:31 +01:00
test mbo 2016-05-20 13:45:50 -07:00
util MPF code simplification 2016-06-02 17:12:24 +01:00