diff options
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/sort_infer.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 92c2e55b1..03f0469bf 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -16,6 +16,7 @@ #include "options/smt_options.h" #include "options/uf_options.h" +#include "smt/dump_manager.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" @@ -65,12 +66,12 @@ PreprocessingPassResult SortInferencePass::applyInternal( assertionsToPreprocess->push_back(nar); } // indicate correspondence between the functions - // TODO (#2308): move this to a better place SmtEngine* smt = smt::currentSmtEngine(); + smt::DumpManager* dm = smt->getDumpManager(); for (const std::pair<const Node, Node>& mrf : model_replace_f) { - smt->setPrintFuncInModel(mrf.first.toExpr(), false); - smt->setPrintFuncInModel(mrf.second.toExpr(), true); + dm->setPrintFuncInModel(mrf.first, false); + dm->setPrintFuncInModel(mrf.second, true); } } // only need to compute monotonicity on the resulting formula if we are |