diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-20 07:52:00 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-20 07:52:00 -0500 |
| commit | 0971aa005c33fb1aaa18ed4522e25d89bb909238 (patch) | |
| tree | 244bb4e0874541abaac9ede3839cd58784d760db /src | |
| parent | d77107cc56b0a089364c3d1512813701c155ea93 (diff) | |
Fix bug 812.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 008514dcc..f462535dd 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -615,7 +615,8 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node } } } - return false; + // spurious if quantifiers engine is in conflict + return p->d_quantEngine->inConflict(); } bool QuantInfo::isPropagatingInstance( QuantConflictFind * p, Node n ) { |