verification errors fixed but DA unsound!!

AndreaKe · AndreaKe · commit 01f7b5270e83 · 2025-12-02T08:19:46.000+01:00
diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
@@ -344,7 +344,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
         return term
 
       val labelNode = getOrCreateAnalysisLabelNode(sourceChunks, sourceTerms)
-      term // XXX ake: labelNode.map(n => Implies(n.term, term)).getOrElse(term)
+      labelNode.map(n => Implies(n.term, term)).getOrElse(term)
     }
 
     def isPathInfeasible(): Boolean = Verifier.config.disableInfeasibilityChecks() && pcs.getCurrentInfeasibilityNode.isDefined

Original file line number	Diff line number	Diff line change
`@@ -344,7 +344,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>`
`344`	`344`	`return term`
`345`	`345`
`346`	`346`	`val labelNode = getOrCreateAnalysisLabelNode(sourceChunks, sourceTerms)`
`347`		`- term // XXX ake: labelNode.map(n => Implies(n.term, term)).getOrElse(term)`
	`347`	`+ labelNode.map(n => Implies(n.term, term)).getOrElse(term)`
`348`	`348`	`}`
`349`	`349`
`350`	`350`	`def isPathInfeasible(): Boolean = Verifier.config.disableInfeasibilityChecks() && pcs.getCurrentInfeasibilityNode.isDefined`