diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/model_postprocessor.cpp | 7 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 20 |
2 files changed, 15 insertions, 12 deletions
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index cbabc9542..c61a61940 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -9,9 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief + ** \brief + ** ** - ** **/ #include "smt/model_postprocessor.h" @@ -92,6 +92,9 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { return n; } NodeBuilder<> b(n.getKind()); + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + b << n.getOperator(); + } TypeNode::iterator t = asType.begin(); for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) { Assert(t != asType.end()); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2505294e4..32d0d1703 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -883,16 +883,16 @@ void SmtEngine::setLogicInternal() throw() { } } // Turn on model-based arrays for QF_AX (unless models are enabled) - if(! options::arraysModelBased.wasSetByUser()) { - if (not d_logic.isQuantified() && - d_logic.isTheoryEnabled(THEORY_ARRAY) && - d_logic.isPure(THEORY_ARRAY) && - !options::produceModels() && - !options::checkModels()) { - Trace("smt") << "turning on model-based array solver" << endl; - options::arraysModelBased.set(true); - } - } + // if(! options::arraysModelBased.wasSetByUser()) { + // if (not d_logic.isQuantified() && + // d_logic.isTheoryEnabled(THEORY_ARRAY) && + // d_logic.isPure(THEORY_ARRAY) && + // !options::produceModels() && + // !options::checkModels()) { + // Trace("smt") << "turning on model-based array solver" << endl; + // options::arraysModelBased.set(true); + // } + // } // Turn on multiple-pass non-clausal simplification for QF_AUFBV if(! options::repeatSimp.wasSetByUser()) { bool repeatSimp = !d_logic.isQuantified() && |