From 3209cd2ded8bfd952cfd99d0398b4c0bd4a0c04d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 23 Jun 2014 16:40:49 +0100 Subject: [PATCH] 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 --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 02ee06985..4f3c73ce6 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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; }