diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index db7c65291..bc335f2df 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -90,7 +90,7 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" #include "theory/substitutions.h" @@ -4512,6 +4512,7 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { quantifiers::SingleInvocationPartition sip; std::vector< Node > funcs; for( unsigned i=0; i<conj[0].getNumChildren(); i++ ){ + // TODO : revisit this when addressing #1205 Node sf = conj[0][i].getAttribute(theory::SygusSynthFunAttribute()); Assert( !sf.isNull() ); funcs.push_back( sf ); |