3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 22:35:35 +00:00
z3/src
Lev 041458f97a fixes the +- bug in gomory cut
Signed-off-by: Lev <levnach@hotmail.com>
2018-09-18 14:42:32 -07:00
..
ackermannization remove spurious copies and inc_refs around ref_vector 2018-06-28 10:31:38 +01:00
api initialize solver before parse is invoked. Fixes issue reported by Selsam 2018-09-13 19:05:45 -07:00
ast fix 2018-09-10 15:15:00 -07:00
cmd_context record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat 2018-08-06 16:21:27 -07:00
math force the new arithmetic solver for QF_LIA 2018-07-09 16:33:48 -07:00
model visit parameters during occurs count 2018-06-29 08:52:25 -07:00
muz Fix is_infty_level to treat 2^16-1 as infinity 2018-09-04 21:49:59 -04:00
nlsat strengthen filter for specialized tactic conditions, add flag to disable hnf to lp_params 2018-07-15 22:35:47 -07:00
opt purify non-constant terms by default to enforce theory 2018-09-10 15:52:02 -07:00
parsers remove some allocs from exceptions 2018-07-02 17:08:02 +01:00
qe update documentation for renamed parameter 2018-07-06 21:25:38 -07:00
sat fix name to divisible, guard under smtlib2_compliant as sugguested in 2018-09-01 18:22:10 -07:00
shell record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat 2018-08-06 16:21:27 -07:00
smt work on Gomory cut 2018-09-18 13:34:05 -07:00
solver narrowing incorrect lemma generation 2018-09-11 11:31:19 -07:00
tactic fix , wronge clausification of negated pb inequalities. Signs were ignored 2018-08-11 13:33:09 -07:00
test disable dotnet in ci script. It seems to get turned on even if dotnet bindings are not requested 2018-09-11 03:14:31 -07:00
util fixes the +- bug in gomory cut 2018-09-18 14:42:32 -07:00
CMakeLists.txt bmc improvements, move fd_solver to self-contained directory 2018-08-05 10:00:49 -07:00