3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 21:20:52 +00:00
z3/src
Nikolaj Bjorner 73662ad60d fix #3016
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-02-15 21:18:15 -10:00
..
ackermannization enhance ackermannize for constant arguments 2019-09-07 16:36:09 +03:00
api Down compatibility for C++03 2020-02-12 10:36:36 -08:00
ast disable automatic coersion to reals 2020-02-11 22:06:04 -08:00
cmd_context fix warnings 2020-01-23 12:14:34 -06:00
math fix #3016 2020-02-15 21:18:15 -10:00
model na 2020-02-11 14:25:25 -08:00
muz fix #3003 2020-02-14 17:51:31 -10:00
nlsat address the NB's comments 2020-01-28 10:04:21 -08:00
opt fix #2945 2020-02-09 15:43:21 -08:00
parsers fix #3015 2020-02-15 21:16:34 -10:00
qe fix #2975, parameter validation to avoid cases where domain of sort is not fixed 2020-02-13 20:20:08 -08:00
sat fix #2974 by using same code path as qe. It now diverges, but this is due to the use of an uninterpreted predicate which the use of mbp doesn't handle 2020-02-13 20:20:08 -08:00
shell move lp_params to smt_params_helper 2020-02-10 11:25:54 -08:00
smt z3str3: assert precondition for regex linearity axiom 2020-02-13 18:19:24 -08:00
solver move to abstract symbols 2020-01-10 12:14:13 -08:00
tactic fix #2976 2020-02-11 22:20:20 -08:00
test fix build of test 2020-02-09 08:25:52 -08:00
util fix #2949 fix #2955 experiment with cut selection 2020-02-08 10:34:14 -08:00
CMakeLists.txt rebase with Z3Prover 2020-01-28 10:04:21 -08:00