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 b51090f78bae41005411dabf89a50df3b6055b5b..e825b60a9c38aa35f2095feadd01aa61525e0905 100644 (file)
--- 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 c9e08b7a8645b9d0d517f5f7af67ad3e4d71223c..2b0108140bf9d1cd8bad82f0d9736a2a18bd7bb1 100644 (file)
--- 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 7e1935bc9ebf7bbbb0cb137294764d3af4f642b4..b8a060cfa73cbd444840e02afcb4d1f51832a7ed 100644 (file)
--- 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 (file)
index 0000000..7caebd5
--- /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)