3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 06:15:37 +00:00
z3/src
Nikolaj Bjorner be50f38903 enforce sign coherence #4740
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-09 14:30:00 -08:00
..
ackermannization add command-line help descriptions on tactics 2020-08-14 19:29:35 -07:00
api Fix reference counting in Z3_mk_fpa_to_ieee_bv 2020-11-06 12:16:09 +00:00
ast tune hoist-rewriter 2020-11-09 11:25:17 -08:00
cmd_context debug arith/mbi 2020-11-02 12:13:19 -08:00
math enforce sign coherence #4740 2020-11-09 14:28:49 -08:00
model mbqi 2020-10-26 11:06:40 -07:00
muz adding dt-solver (#4739) 2020-10-18 15:28:21 -07:00
nlsat pass algebraic manager to arith-plugin mk-numeral because rational check may overwrite the argument using the current manager deals with crash as part of #4532 2020-07-26 17:52:28 -07:00
opt delay internalize (#4714) 2020-09-28 19:24:16 -07:00
params add parameter for scenario from #4743 2020-10-30 01:14:34 -07:00
parsers fix #4594 2020-07-27 09:22:53 -07:00
qe redo purification 2020-10-29 11:06:31 -07:00
sat TB08-009 fix z3 build on windows (#4782) 2020-11-08 20:47:25 -08:00
shell fix #4763: shell not finishing before hard timeout 2020-10-30 10:01:09 +00:00
smt enforce sign coherence #4740 2020-11-09 14:30:00 -08:00
solver debug arith/mbi 2020-11-02 12:13:19 -08:00
tactic tune hoist-rewriter 2020-11-09 11:25:18 -08:00
test adding dt-solver (#4739) 2020-10-18 15:28:21 -07:00
util Fix bonus subtraction in fp.rem. Fixes #4564. Fixes most of #2381. 2020-11-06 20:54:10 +00:00
CMakeLists.txt mbp (#4741) 2020-10-21 15:48:40 -07:00