diff options
Diffstat (limited to 'src/preprocessing')
| -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 31f927359..7336ac159 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, // make a separate smt call std::unique_ptr<SmtEngine> rrSygus; theory::initializeSubsolver(rrSygus); - 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; |