diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-11 15:07:37 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-11 15:07:37 -0600 |
| commit | 7acc2844df65ab6fdbf8166653c71eaa26d4d151 (patch) | |
| tree | e289c79b5cf0bde3f7e261f81fc5c54c58b0ae01 /src/theory/quantifiers/full_model_check.cpp | |
| parent | 78608a5925938d7ae78b5ac08d2f003d7332810a (diff) | |
More aggressive conditional rewriting for quantified formulas. Bug fix set incomplete for fmc.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 00a5241f5..ff0da13e1 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -819,8 +819,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No } } d_addedLemmas += addedLemmas; - Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl; - return true; + Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl; + return addedLemmas>0 || !riter.d_incomplete; }else{ Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl; return false; |