diff options
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 12edaa31c..951a6b545 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -131,6 +131,9 @@ void TheoryQuantifiers::check(Effort e) { break; case kind::INST_CLOSURE: getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); + if( !options::lteRestrictInstClosure() ){ + getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] ); + } break; case kind::EQUAL: //do nothing |