diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-16 11:07:36 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-16 11:07:36 +0200 |
commit | 548582b252170f35a602705a109d88a608611cca (patch) | |
tree | abcfe42578de4b4a99905ed76e1df23c396820ef /src/smt | |
parent | bad7f4fe4dca4c6511c2862bf81b6791640ac78f (diff) |
Add option --fmf-fun-rlv, remove deprecated option --axiom-inst.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 7 |
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 ); |