Fix for new CASC features, fixes Java builds.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 247c367b4e430a1561b2189d047b10fe3b6bf578..28a45206f80be3a7f0f86dc7dc3b84c7f4e4a372 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3020,8 +3020,8 @@ void SmtEnginePrivate::processAssertions() {
     SortInference * si = d_smt.d_theoryEngine->getSortInference();
     si->simplify( d_assertionsToPreprocess );
     for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){
-      d_smt.setPrintFuncInModel( it->first, false );
-      d_smt.setPrintFuncInModel( it->second, true );
+      d_smt.setPrintFuncInModel( it->first.toExpr(), false );
+      d_smt.setPrintFuncInModel( it->second.toExpr(), true );
     }
   }
 
@@ -4125,14 +4125,13 @@ void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) {
   d_theoryEngine->setUserAttribute(attr, expr.getNode());
 }
 
-void SmtEngine::setPrintFuncInModel( Node f, bool p ) {
+void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
   Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
-  Expr fe = f.toExpr();
   for( unsigned i=0; i<d_modelGlobalCommands.size(); i++ ){
     Command * c = d_modelGlobalCommands[i];
     DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
     if(dfc != NULL) {
-      if( dfc->getFunction()==fe ){
+      if( dfc->getFunction()==f ){
         dfc->setPrintInModel( p );
       }
     }
@@ -4141,7 +4140,7 @@ void SmtEngine::setPrintFuncInModel( Node f, bool p ) {
     Command * c = (*d_modelCommands)[i];
     DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
     if(dfc != NULL) {
-      if( dfc->getFunction()==fe ){
+      if( dfc->getFunction()==f ){
         dfc->setPrintInModel( p );
       }
     }

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c53156a3cb7a6ba9d808bdd746d20e9ab7880c3a..acf7954bc6721328889ca36e0c870f8860268c49 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -656,7 +656,7 @@ public:
   /**
    * Set print function in model
    */
-  void setPrintFuncInModel( Node f, bool p );
+  void setPrintFuncInModel(Expr f, bool p);
   
 };/* class SmtEngine */