More strictly constraining wildcards in MCE (#829)

marcoeilers · web-flow · commit 5e3ab014b112 · 2024-03-29T20:06:16.000+01:00
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)

Original file line number	Diff line number	Diff line change
`@@ -360,7 +360,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {`
`360`	`360`
`361`	`361`	`val constraint = And(IsValidPermVar(permTaken),`
`362`	`362`	`PermAtMost(permTaken, ch.perm),`
`363`		`- Implies(Not(eq), permTaken === NoPerm)`
	`363`	`+ Implies(Not(eq), permTaken === NoPerm),`
	`364`	`+ Implies(And(eq, IsPositive(ch.perm)), PermLess(permTaken, ch.perm))`
`364`	`365`	`)`
`365`	`366`
`366`	`367`	`v.decider.assume(constraint)`