diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-16 19:06:05 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-16 19:06:16 -0500 |
| commit | 349c84b95cea084f28ff637c7cd4e99710692aeb (patch) | |
| tree | 64f4b2da4c3f14a82da30a08152fc82f83dfb5a7 /src/theory/quantifiers/quant_conflict_find.cpp | |
| parent | 976ee5b66b7584b9fe46eab1facf5e5f857e723f (diff) | |
Use matching heuristics for EPR instantiation.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index bac2aa35c..522f4dfce 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1853,7 +1853,7 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledBoolConnective( TNode n ) { - return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ); + return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ) && n.getKind()!=SEP_STAR; } bool MatchGen::isHandledUfTerm( TNode n ) { |