Fix for fmf-fun when the option is set by user command.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 94ff5d9b3703f010a7c27bf851653250c15faa69..1407daadc77d2e505bbab43327b89453f8edcca3 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1042,9 +1042,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_context->push();
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
-  if( options::fmfFunWellDefined() || options::fmfFunWellDefinedRelevant() ){
-    d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext);
-  }
+  d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext);
   d_modelCommands = new(true) smt::CommandList(d_userContext);
 }
 
@@ -1191,10 +1189,7 @@ SmtEngine::~SmtEngine() throw() {
     }
 
     d_definedFunctions->deleteSelf();
-
-    if( d_fmfRecFunctionsDefined != NULL ){
-      d_fmfRecFunctionsDefined->deleteSelf();
-    }
+    d_fmfRecFunctionsDefined->deleteSelf();
 
     delete d_theoryEngine;
     d_theoryEngine = NULL;
@@ -4185,6 +4180,7 @@ void SmtEnginePrivate::processAssertions() {
     //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
     if( options::fmfFunWellDefined() ){
       quantifiers::FunDefFmf fdf;
+      Assert( d_smt.d_fmfRecFunctionsDefined!=NULL );
       //must carry over current definitions (for incremental)
       for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin();
            fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) {

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 730108ee793ee6717626f30f2b8a71f1a7ff585a..0c13961cc6c1e64b6cb4f440a04b06b76741a3c2 100644 (file)
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -70,7 +70,8 @@ TESTS =       \
        bug652.smt2 \
        bug782.smt2 \
        quant_real_univ.cvc \
-       constr-ground-to.smt2
+       constr-ground-to.smt2 \
+       bug-041417-set-options.cvc
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/fmf/bug-041417-set-options.cvc b/test/regress/regress0/fmf/bug-041417-set-options.cvc
new file mode 100644 (file)
index 0000000..16f59f7
--- /dev/null
+++ b/test/regress/regress0/fmf/bug-041417-set-options.cvc
@@ -0,0 +1,16 @@
+% EXPECT: invalid
+OPTION "finite-model-find";
+OPTION "fmf-fun";
+
+DATATYPE
+  Node = A | B
+END;
+
+link, reach: (Node,Node,INT) -> BOOLEAN;
+
+ASSERT FORALL(x,y:Node, c:INT):
+  link(x,y,c) => reach(x,y,c);
+
+ASSERT link(A,B,1);
+
+QUERY reach(A,B,5);