mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Disabled construction of partial model on theory failure as it caused buggy behavior.
Thanks to parno (Codeplex Issue #117)! Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
000db81b4f
commit
3209cd2ded
|
@ -3945,7 +3945,7 @@ namespace smt {
|
|||
m_fingerprints.display(tout);
|
||||
);
|
||||
failure fl = get_last_search_failure();
|
||||
if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) {
|
||||
if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == THEORY) {
|
||||
// don't generate model.
|
||||
return;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue