Skip to content

Commit bedaee1

Browse files
committed
nodes with failed obligations are always explicit assumptions
1 parent 392473c commit bedaee1

1 file changed

Lines changed: 3 additions & 0 deletions

File tree

src/main/scala/dependencyAnalysis/DependencyAnalyzer.scala

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -359,8 +359,11 @@ class DefaultDependencyAnalyzer(member: ast.Member) extends DependencyAnalyzer {
359359
}
360360

361361
override def addAssertionFailedNode(failedAssertion: Term, assertionType: AssumptionType, sourceInfo: AnalysisSourceInfo): Option[Int] = {
362+
val assumeNode = SimpleAssumptionNode(failedAssertion, None, sourceInfo, AssumptionType.Explicit, isClosed=false, isJoinNode=false)
362363
val assertFailedNode = SimpleAssertionNode(failedAssertion, assertionType, sourceInfo, isClosed=false, hasFailed=true)
364+
dependencyGraph.addNode(assumeNode)
363365
dependencyGraph.addNode(assertFailedNode)
366+
dependencyGraph.addEdges(Set(assumeNode.id), assertFailedNode.id)
364367
Some(assertFailedNode.id)
365368
}
366369

0 commit comments

Comments
 (0)