3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
z3/src
Lev Nachmanson 6d8e5400fd return an empty model when the status of the solver is neither FEASIBLE nor OPTIMAL
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-16 12:58:39 -07:00
..
ackermannization fix #3557 2020-04-03 16:37:59 -07:00
api fix #3931 2020-04-12 15:37:18 -07:00
ast warnings 2020-04-15 17:13:02 -07:00
cmd_context fix #3985 2020-04-16 12:04:46 -07:00
math return an empty model when the status of the solver is neither FEASIBLE nor OPTIMAL 2020-04-16 12:58:39 -07:00
model fix #3908 2020-04-11 13:58:10 -04:00
muz warnings 2020-04-15 17:13:02 -07:00
nlsat bool_vector, some spacer tidy 2020-04-05 12:59:04 -07:00
opt fix #3950 2020-04-15 15:07:53 -07:00
parsers fix #3474 2020-03-22 20:40:34 -07:00
qe fix #3975 2020-04-15 08:06:43 -07:00
sat fix #3953 2020-04-14 09:43:03 -07:00
shell fix #3938 2020-04-13 13:05:53 -07:00
smt fix #3979 2020-04-16 10:54:19 -07:00
solver add missing fixed propagations on negated integer inequalities 2020-04-11 02:28:38 -07:00
tactic fix #3948 - cache has to be reset also when processing 'and' because it could be processed in an incompatible context by the caller 2020-04-15 13:29:45 -07:00
test change lar_terms to use column indices 2020-04-06 12:13:59 -07:00
util na 2020-04-15 12:25:07 -07:00
CMakeLists.txt Julia bindings (#3228) 2020-03-10 09:16:34 -07:00