From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 23 Feb 2022 20:59:37 +0000 (-0600)
Subject: Do not insist that entries for UF are constant in FMF (#8140)
X-Git-Tag: cvc5-1.0.0~394
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=357c5e8b2ee1a9f08d3bca96fc1dc821c80943d9;p=cvc5.git

Do not insist that entries for UF are constant in FMF (#8140)

Fixes #8096.
---

diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index b51090f78..e825b60a9 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -121,7 +121,6 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix)
     size_t ii = (ncond - 1) - i;
     Node v = odef->d_value[ii];
     Trace("fmc-model-func") << "Value is : " << v << std::endl;
-    Assert(v.isConst());
     if (curr.isNull())
     {
       Trace("fmc-model-func") << "base : " << v << std::endl;
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index c9e08b7a8..2b0108140 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -488,7 +488,6 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
           << "Representative of " << v << " is " << nv << std::endl;
       if( !nv.isConst() ){
         Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
-        Assert(false);
       }
       Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
       if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7e1935bc9..b8a060cfa 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1805,6 +1805,7 @@ set(regress_1_tests
   regress1/fmf/issue6690-re-enum.smt2
   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/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/ko-bound-set.cvc.smt2
diff --git a/test/regress/regress1/fmf/issue8096-non-const-rep.smt2 b/test/regress/regress1/fmf/issue8096-non-const-rep.smt2
new file mode 100644
index 000000000..7caebd54b
--- /dev/null
+++ b/test/regress/regress1/fmf/issue8096-non-const-rep.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp -q
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (= 1 (* (str.len (str.replace_all a a b)) (- (str.len (str.from_code (str.len b))) 1))))
+(check-sat)