Add option --fmf-fun-rlv, remove deprecated option --axiom-inst.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4874b076e..0af5c7fc1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -739,7 +739,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_context->push();
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
-  if( options::fmfFunWellDefined() ){
+  if( options::fmfFunWellDefined() || options::fmfFunWellDefinedRelevant() ){
     d_fmfRecFunctionsAbs = new(true) TypeNodeMap(d_userContext);
     d_fmfRecFunctionsConcrete = new(true) NodeListMap(d_userContext);
   }
@@ -1364,6 +1364,11 @@ void SmtEngine::setDefaults() {
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
+  if( options::fmfFunWellDefinedRelevant() ){
+    if( !options::fmfFunWellDefined.wasSetByUser() ){
+      options::fmfFunWellDefined.set( true );
+    }
+  }
   if( options::fmfFunWellDefined() ){
     if( !options::finiteModelFind.wasSetByUser() ){
       options::finiteModelFind.set( true );