diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-08 23:54:18 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-08 23:54:18 +0000 |
commit | 2979089be3bc655d8bdd6245e193f356b4f7c93c (patch) | |
tree | ddb51fd7df95a39e7c67c3c08a3c6cbd3cc9ff42 /src/smt | |
parent | 44ac537312dcba8fc179f5ea9489e8cd7266f71c (diff) |
Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases for division by 0.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7fcb64219..24d6fb0b4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -661,6 +661,15 @@ 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_UF)){ + d_logic = d_logic.getUnlockedCopy(); + d_logic.enableTheory(theory::THEORY_UF); + d_logic.lock(); + } + // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) { |