Always assign function values in higher order (#4279)

Fixes #4277.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 844d253798f089c1e663689dfa804dd0a6d636d3..531dfa512ebfe3d7b02791c7d1eebd57ac63fe37 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -864,6 +864,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       // by default, use store axioms only if --ho-elim is set
       options::hoElimStoreAx.set(options::hoElim());
     }
+    if (!options::assignFunctionValues())
+    {
+      // must assign function values
+      options::assignFunctionValues.set(true);
+    }
     // Cannot use macros, since lambda lifting and macro elimination are inverse
     // operations.
     if (options::macrosQuant())

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index e96bee4103569c88bc3207f527346f48efa2eec9..10e57e7949d6c36321e78f0d0e6976d3096ab917 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -34,6 +34,8 @@ TheoryModel::TheoryModel(context::Context* c,
       d_using_model_core(false),
       d_enableFuncModels(enableFuncModels)
 {
+  // must use function models when ufHo is enabled
+  Assert(d_enableFuncModels || !options::ufHo());
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3c104862fdb5d9b6c87a5ea3f7199b46f61db425..19ccc91e4cac4222b2ae8f3c7562dcdc31cdaa5b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -501,6 +501,7 @@ set(regress_0_tests
   regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
   regress0/fp/issue3536.smt2
+  regress0/fp/issue4277-assign-func.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/rti_3_5_bug_report.smt2
   regress0/fp/simple.smt2

diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2
new file mode 100644 (file)
index 0000000..5c39abc
--- /dev/null
+++ b/test/regress/regress0/fp/issue4277-assign-func.smt2
@@ -0,0 +1,10 @@
+; REQUIRES: symfpu
+(set-logic ALL)
+(set-option :uf-ho true)
+(set-option :assign-function-values false)
+(set-info :status sat)
+(declare-fun b () (_ BitVec 1))
+(declare-fun c () (_ BitVec 8))
+(declare-fun d () (_ BitVec 23))
+(assert (= 0 (fp.to_real (fp b c d))))
+(check-sat)