diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-14 15:36:28 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-14 15:36:28 -0500 |
| commit | 1138911e0af7c15a7b41a5d02ff3edab2c837449 (patch) | |
| tree | 6b7a70bd32d461cff687f11def74bab0447aad82 /src/theory/quantifiers/full_model_check.cpp | |
| parent | b71bbbbc607b5ca0c2bec8b8cf6c7af596d21997 (diff) | |
Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). Improve datatypes rewrite, make option for previous dt semantics.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 6c889781d..126b30b81 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -937,7 +937,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n void FullModelChecker::doNegate( Def & dc ) { for (unsigned i=0; i<dc.d_cond.size(); i++) { if (!dc.d_value[i].isNull()) { - dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true; + dc.d_value[i] = dc.d_value[i]==d_true ? d_false : ( dc.d_value[i]==d_false ? d_true : dc.d_value[i] ); } } } |