From 5272f5d02f109b7dbfdb5088a1efbf7d13b64487 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 31 Mar 2020 11:49:02 -0500 Subject: [PATCH] Fix strange bound regression (#4192) Several things have happened with this regression lately, in chronological order: (1) Instantiations involving bounded set quantifiers were changed to use choice to represent symbolic instantiations, (2) fmf-bound was decoupled from finite-model-find (the latter is not enabled when the former is), (3) choice was set to be an "unevaluated" kind (in 0060de3). After (1) and (2), for the regression test/regress/regress1/fmf/fmf-strange-bounds.smt2, CVC4 was answering "sat" correctly but internally there was a source of incompleteness. In particular, a choice term was being generated in an instantiation that was later incorrectly evaluated, thus allowing CVC4 to skip an instantiation it shouldn't have. The recent commit of (3) resolved this issue, making it so that choice is not an evaluated kind. This meant the benchmark went "sat" -> "unknown". This PR fixes this issue by enabling --finite-model-find, which is now necessary to answer "sat". It also adds a further test quantifier that was used in debugging this issue. Fixes regress1. --- test/regress/regress1/fmf/fmf-strange-bounds.smt2 | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/test/regress/regress1/fmf/fmf-strange-bounds.smt2 b/test/regress/regress1/fmf/fmf-strange-bounds.smt2 index 7812c2431..bdbca4bd0 100644 --- a/test/regress/regress1/fmf/fmf-strange-bounds.smt2 +++ b/test/regress/regress1/fmf/fmf-strange-bounds.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-bound +; COMMAND-LINE: --fmf-bound --finite-model-find ; EXPECT: sat (set-logic ALL) (set-info :status sat) @@ -23,6 +23,12 @@ (=> (and (<= 0 y) (<= y (h z))) (P x y z)))))) +(assert (forall ((x Int) (y Int) (z U)) (=> +(or (= x 5) (= x 6)) +(=> (and (<= 0 y) (<= y x)) +(P x y z))))) + + (declare-fun Q (U Int) Bool) (declare-const a U) -- 2.30.2