From 7461cd576c0ad4c19e996644157a63920c67649b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 27 Oct 2021 13:40:18 -0500 Subject: Fix care graph computation for higher-order (#7474) Since we apply a lazy schema for app completion, this may omit terms from the care graph that are relevant for theory combination. This corrects the care graph for UF when higher-order is enabled by considering the HO_APPLY version of all partially and fully applied prefixes of APPLY_UF terms during TheoryUF::computeCareGraph. Fixes #5741. Fixes #5744. Fixes #5201. Fixes #5078. Fixes #4758. --- test/regress/regress0/ho/issue5744-cg-model.smt2 | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test/regress/regress0/ho/issue5744-cg-model.smt2 (limited to 'test/regress/regress0/ho/issue5744-cg-model.smt2') diff --git a/test/regress/regress0/ho/issue5744-cg-model.smt2 b/test/regress/regress0/ho/issue5744-cg-model.smt2 new file mode 100644 index 000000000..5650351cd --- /dev/null +++ b/test/regress/regress0/ho/issue5744-cg-model.smt2 @@ -0,0 +1,7 @@ +(set-logic HO_ALL) +(set-info :status sat) +(declare-fun r4 () Real) +(declare-fun ufrb5 (Real Real Real Real Real) Bool) +(assert (ufrb5 0.0 0.0 0.0 0.0 0)) +(assert (ufrb5 (+ r4 r4) 0.0 1 0.0 0.0)) +(check-sat) -- cgit v1.2.3