From a7091c61d6661079cfef6b489809579a0c6ac792 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 17 Jul 2012 21:01:06 +0000 Subject: [PATCH] fix for --produce-models with CVC4 presentation language --- src/smt/smt_engine.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 01ce73be1..a182d8927 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1889,6 +1889,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { void SmtEngine::addToModelType( Type& t ){ Trace("smt") << "SMT addToModelType(" << t << ")" << endl; SmtScope smts(this); + finalOptionsAreSet(); if( Options::current()->produceModels ) { d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) ); } @@ -1897,6 +1898,7 @@ void SmtEngine::addToModelType( Type& t ){ void SmtEngine::addToModelFunction( Expr& e ){ Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl; SmtScope smts(this); + finalOptionsAreSet(); if( Options::current()->produceModels ) { d_theoryEngine->getModel()->addDefineFunction( e.getNode() ); } -- 2.30.2