From 88ef1f0be6bd712cf1ce8401416d634f61f381b4 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Thu, 15 Nov 2012 20:57:22 +0000 Subject: [PATCH] forgot to uncomment setLogicInternal for THEORY_BV --- src/smt/smt_engine.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 69aec695c..425892583 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -720,8 +720,8 @@ void SmtEngine::setLogicInternal() throw() { d_logic.lock(); // may need to force uninterpreted functions to be on for non-linear - if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) /*|| - d_logic.isTheoryEnabled(theory::THEORY_BV)*/) && + if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) || + d_logic.isTheoryEnabled(theory::THEORY_BV)) && !d_logic.isTheoryEnabled(theory::THEORY_UF)){ d_logic = d_logic.getUnlockedCopy(); d_logic.enableTheory(theory::THEORY_UF); -- 2.30.2