Do not assign higher-order representative if function does not exist (#4073)

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index bf0a82a204e90a19d3ccaa30e97f8a0dbfde102f..7bfb0e8f3ed9c8c7a9f23d33262293d965eb3844 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -669,8 +669,8 @@ bool TheoryModel::areFunctionValuesEnabled() const
 }
 
 void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
-  Assert(d_uf_models.find(f) == d_uf_models.end());
   Trace("model-builder") << "  Assigning function (" << f << ") to (" << f_def << ")" << endl;
+  Assert(d_uf_models.find(f) == d_uf_models.end());
 
   if( options::ufHo() ){
     //we must rewrite the function value since the definition needs to be a constant value
@@ -685,9 +685,9 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
     d_uf_models[f] = f_def;
   }
 
-  if( options::ufHo() ){
+  if (options::ufHo() && d_equalityEngine->hasTerm(f))
+  {
     Trace("model-builder-debug") << "  ...function is first-class member of equality engine" << std::endl;
-    Assert(d_equalityEngine->hasTerm(f));
     // assign to representative if higher-order
     Node r = d_equalityEngine->getRepresentative( f );
     //always replace the representative, since it is initially assigned to itself

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fd4f2aef092dad55727ca14f28aec421ffe0d2e0..be96ca70d0456eb5d00cd6be535f9138bbb80e40 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1300,6 +1300,7 @@ set(regress_1_tests
   regress1/gensys_brn001.smt2
   regress1/ho/fta0328.lfho.p
   regress1/ho/issue3136-fconst-bool-bool.smt2
+  regress1/ho/issue4065-no-rep.smt2
   regress1/ho/nested_lambdas-AGT034^2.smt2
   regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
   regress1/ho/NUM638^1.smt2

diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2
new file mode 100644 (file)
index 0000000..841d050
--- /dev/null
+++ b/test/regress/regress1/ho/issue4065-no-rep.smt2
@@ -0,0 +1,10 @@
+(set-logic AUFBV)
+(set-info :status sat)
+(set-option :bv-div-zero-const false)
+(set-option :fmf-bound-int true)
+(set-option :uf-ho true)
+(declare-fun _substvar_20_ () Bool)
+(declare-sort S4 0)
+(assert (forall ((q15 S4) (q16 (_ BitVec 20)) (q17 (_ BitVec 13))) (xor (= (_ bv0 13) (_ bv0 13) q17 (bvsrem (_ bv0 13) (_ bv0 13)) q17) _substvar_20_ true)))
+(check-sat)
+(exit)