From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Feb 2022 16:27:16 +0000 (-0600)
Subject: Remove spurious assertion involving constants for arguments to UF from FMF (#8168)
X-Git-Tag: cvc5-1.0.0~378
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=81412133512647fed893dc8f0a6cfdbe09d407da;p=cvc5.git

Remove spurious assertion involving constants for arguments to UF from FMF (#8168)

Fixes #8163.
---

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 2b0108140..42901b958 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -478,7 +478,6 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
           Trace("fmc-warn") << "Warning : model for " << op
                             << " has non-constant argument in model " << ri
                             << " (from " << ci << ")" << std::endl;
-          Assert(false);
         }
         entry_children.push_back(ri);
       }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3afba62b7..64e933ff9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1822,6 +1822,7 @@ set(regress_1_tests
   regress1/fmf/issue6744-2-unc-bool-var.smt2
   regress1/fmf/issue6744-3-unc-bool-var.smt2
   regress1/fmf/issue8096-non-const-rep.smt2
+  regress1/fmf/issue8163-nconst-arg.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/ko-bound-set.cvc.smt2
diff --git a/test/regress/regress1/fmf/issue8163-nconst-arg.smt2 b/test/regress/regress1/fmf/issue8163-nconst-arg.smt2
new file mode 100644
index 000000000..4d8c03e7a
--- /dev/null
+++ b/test/regress/regress1/fmf/issue8163-nconst-arg.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun b (Real) Real)
+(assert (forall ((_2 Bool)) (= _2 (and _2 (= 0.0 (b (exp 1.0)))))))
+(check-sat)