diff options
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 7ad2c54eb..7773b05d5 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -19,6 +19,8 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/quantifiers/lazy_trie.h" #include "util/bitvector.h" #include "util/random.h" @@ -820,8 +822,8 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr) return; } // we have detected unsoundness in the rewriter - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - std::ostream* out = nodeManagerOptions.getOut(); + Options& sopts = smt::currentSmtEngine()->getOptions(); + std::ostream* out = sopts.getOut(); (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl; // debugging information (*out) << "Terms are not equivalent for : " << std::endl; |