diff options
Diffstat (limited to 'src/smt/sygus_solver.cpp')
| -rw-r--r-- | src/smt/sygus_solver.cpp | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 240f96af7..32a0ee220 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -25,8 +25,6 @@ #include "options/option_exception.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" -#include "printer/printer.h" -#include "smt/dump.h" #include "smt/preprocessor.h" #include "smt/smt_solver.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -211,10 +209,6 @@ Result SygusSolver::checkSynth(Assertions& as) Trace("smt") << "...constructed forall " << body << std::endl; Trace("smt") << "Check synthesis conjecture: " << body << std::endl; - if (Dump.isOn("raw-benchmark")) - { - d_env.getPrinter().toStreamCmdCheckSynth(d_env.getDumpOut()); - } d_sygusConjectureStale = false; |