diff options
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 4500c7880..2ffe7e0ce 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -303,7 +303,7 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions, SmtEngine* currSmt = smt::currentSmtEngine(); SmtEngine rrSygus(nm->toExprManager(), &currSmt->getOptions()); rrSygus.setLogic(currSmt->getLogicInfo()); - rrSygus.assertFormula(body.toExpr()); + rrSygus.assertFormula(body); Trace("sygus-infer") << "*** Check sat..." << std::endl; Result r = rrSygus.checkSat(); Trace("sygus-infer") << "...result : " << r << std::endl; |