diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 11:28:25 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 11:28:25 -0400 |
| commit | b01a91bb5690b2648a5b8d91f940a6746cba34a3 (patch) | |
| tree | 9c4881ead1f7bce2bdd522765a648b6ed896d5c3 /src/theory/quantifiers/full_model_check.cpp | |
| parent | 3fc61e7f2b84765dc547634463198b30516ed432 (diff) | |
| parent | 698f5a09b1c0177abfd2eaa2b110de100fd108ef (diff) | |
Merge remote-tracking branch 'upstream/master' into sets
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 3b6c8e492..0f3e53827 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] ); } } } |