From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 14 Apr 2017 16:06:45 +0000 (-0500)
Subject: Fix for fmf-fun when the option is set by user command.
X-Git-Tag: cvc5-1.0.0~5837
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8748256b518f5ad4b1cefe46d9445b562199871c;p=cvc5.git

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 94ff5d9b3..1407daadc 100644
--- 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 730108ee7..0c13961cc 100644
--- 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
index 000000000..16f59f78c
--- /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);