From 357c5e8b2ee1a9f08d3bca96fc1dc821c80943d9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Feb 2022 14:59:37 -0600 Subject: [PATCH] Do not insist that entries for UF are constant in FMF (#8140) Fixes #8096. --- src/theory/quantifiers/fmf/first_order_model_fmc.cpp | 1 - src/theory/quantifiers/fmf/full_model_check.cpp | 1 - test/regress/CMakeLists.txt | 1 + test/regress/regress1/fmf/issue8096-non-const-rep.smt2 | 8 ++++++++ 4 files changed, 9 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/fmf/issue8096-non-const-rep.smt2 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) -- 2.30.2