diff options
Diffstat (limited to 'src/theory/quantifiers/fun_def_evaluator.cpp')
| -rw-r--r-- | src/theory/quantifiers/fun_def_evaluator.cpp | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index 83debe0d9..376d0eb47 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -150,17 +150,10 @@ Node FunDefEvaluator::evaluate(Node n) const ret = nm->mkNode(cur.getKind(), children); ret = Rewriter::rewrite(ret); } - if (!ret.isConst()) - { - Trace("fd-eval") << "FunDefEvaluator: non-constant subterm " << ret - << ", FAIL" << std::endl; - // failed, possibly due to free variable - return Node::null(); - } visited[cur] = ret; } } - else if (!curEval.isConst()) + else if (cur != curEval && !curEval.isConst()) { Trace("fd-eval-debug") << "from body " << cur << std::endl; // we had to evaluate our body, which should have a definition now @@ -168,7 +161,6 @@ Node FunDefEvaluator::evaluate(Node n) const Assert(it != visited.end()); // our definition is the result of the body visited[cur] = it->second; - Assert(it->second.isConst()); } } } while (!visit.empty()); |