From 45d96ce6cdd0eb5a899611b4b0be243c6887da39 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 29 Oct 2012 18:25:48 +0000 Subject: [PATCH] Tweak to options configuration for turning off minisat elimination when models are on --- src/smt/smt_engine.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ca8417dea..7fcb64219 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -836,7 +836,7 @@ void SmtEngine::setLogicInternal() throw() { //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ - if( d_logic.isQuantified() || options::produceModels() ){ + if( d_logic.isQuantified() || options::produceModels() || options::checkModels() ){ options::minisatUseElim.set( false ); } } -- 2.30.2