diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-06 17:30:53 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-06 17:30:53 -0600 |
| commit | babbe0e30d769b5f68cb3f36820fbb5e176de7c5 (patch) | |
| tree | 3b0195271c8fdf233836ccd726e4f2c6cd03865c /src/smt/smt_engine.cpp | |
| parent | ea4355639142f10a2bc5c1aa6044d9bbc246435b (diff) | |
Generalize containsQuantifiers to hasClosure (#3722)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 83d8fb612..6a63a991f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -95,7 +95,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/sygus_abduct.h" #include "theory/quantifiers/sygus/synth_engine.h" @@ -4828,7 +4827,7 @@ void SmtEngine::checkModel(bool hardFailure) { // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas if( hardFailure && !n.isConst() && n.getKind() != kind::LAMBDA ){ Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl; - AlwaysAssert(quantifiers::QuantifiersRewriter::containsQuantifiers(n)); + AlwaysAssert(expr::hasClosure(n)); Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n << endl; continue; } |