From ccab28cc44cfa57f027780bb29160f7f1195d3ee Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 4 Feb 2025 10:40:23 +0100 Subject: [PATCH] Fixing issue #896 (#898) --- .../rules/MoreCompleteExhaleSupporter.scala | 2 +- .../resources/moreCompleteExhale/0896.vpr | 25 +++++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 src/test/resources/moreCompleteExhale/0896.vpr diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index dacbeacea..f23874143 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -130,7 +130,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { case Some(v) => ReusedSummarisingSnapshot(v) case None => - val ss = v.decider.appliedFresh("ss", sort, s.functionRecorderQuantifiedVariables().map(_._1)) + val ss = v.decider.appliedFresh("ss", sort, s.functionRecorderQuantifiedVariables().map(_._1) ++ s.quantifiedVariables.map(_._1)) FreshSummarisingSnapshot(ss) } } diff --git a/src/test/resources/moreCompleteExhale/0896.vpr b/src/test/resources/moreCompleteExhale/0896.vpr new file mode 100644 index 000000000..7d8dfc80d --- /dev/null +++ b/src/test/resources/moreCompleteExhale/0896.vpr @@ -0,0 +1,25 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +field f: Int + +predicate P(x: Ref) { + acc(x.f) +} + +method foo(x: Ref, y: Ref) +{ + inhale acc(x.f) && x.f == 4 && acc(y.f) && y.f == 5 + fold P(x) + fold P(y) + + var myseq: Seq[Ref] := Seq(x, y) + + assert forall r: Ref :: {r in myseq} r in myseq ==> unfolding P(r) in r.f > 2 + + assert x in myseq + assert y in myseq + + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} \ No newline at end of file