Add --no-condense-function-values option for explicit function models (useful in some applications)

1 files changed, 5 insertions, 2 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 1c511be30..544ee6c85 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -19,6 +19,7 @@
 #include "smt/options.h"
 #include "smt/smt_engine.h"
 #include "theory/uf/theory_uf_model.h"
+#include "theory/uf/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -851,8 +852,10 @@ void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
           default_v = (*te);
         }
         ufmt.setDefaultValue( m, default_v );
-        ufmt.simplify();
-        Node val = ufmt.getFunctionValue( "_ufmt_" );
+        if(options::condenseFunctionValues()) {
+          ufmt.simplify();
+        }
+        Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() );
         Trace("model-builder") << "  Assigning (" << n << ") to (" << val << ")" << endl;
         m->d_uf_models[n] = val;
         //ufmt.debugPrint( std::cout, m );