More strictly constraining wildcards in MCE (viperproject#829)

viper-admin · Mar 29, 2024 · 5e3ab01 · 5e3ab01
1 parent b1c2311
commit 5e3ab01
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -360,7 +360,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
         val constraint = And(IsValidPermVar(permTaken),
           PermAtMost(permTaken, ch.perm),
-          Implies(Not(eq), permTaken === NoPerm)
+          Implies(Not(eq), permTaken === NoPerm),
+          Implies(And(eq, IsPositive(ch.perm)), PermLess(permTaken, ch.perm))
         )
 
         v.decider.assume(constraint)