Do not make models for quantified function variables (#4039)

If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 2b7f78008f748e73b2f95994aabd1d877855db21..1498e54a657f5f3f9fc317db1014a4c0d7b7f8cb 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -356,8 +356,14 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) {
 
 void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
   if( n.getKind()==APPLY_UF ){
-    if( d_models.find(n.getOperator())==d_models.end()) {
-      d_models[n.getOperator()] = new Def;
+    // cannot be a bound variable
+    Node op = n.getOperator();
+    if (op.getKind() != BOUND_VARIABLE)
+    {
+      if (d_models.find(op) == d_models.end())
+      {
+        d_models[op] = new Def;
+      }
     }
   }
 }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b282e69110680ec14d81f346a37958a38e1a1760..de2091ef6f156ee59bb94a56954fb8914fd88552 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1860,6 +1860,7 @@ set(regress_1_tests
   regress1/sygus/issue3839-cond-rewrite.smt2
   regress1/sygus/issue3944-div-rewrite.smt2
   regress1/sygus/issue3947-agg-miniscope.smt2
+  regress1/sygus/issue3995-fmf-var-op.smt2
   regress1/sygus/issue4009-qep.smt2
   regress1/sygus/issue4025-no-rlv-cond.smt2
   regress1/sygus/large-const-simp.sy

diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
new file mode 100644 (file)
index 0000000..72ece40
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inference --fmf-bound --uf-ho --no-bv-div-zero-const
+(set-logic ALL)
+(declare-fun a () (_ BitVec 1))
+(assert (bvsgt (bvsmod a a) #b0))
+(check-sat)