Marking HasDomain terms as global to fix issue #954

marcoeilers · marcoeilers · commit 365bb085cbae · 2025-12-02T17:17:49.000+01:00
diff --git a/silver b/silver
@@ -1 +1 @@
-Subproject commit e61ca81bd46612a5e126c40b757fe27966965b7e
+Subproject commit e7ce7757caff264b17e54f5c4fecedc77862c9ad
diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
@@ -679,6 +679,7 @@ object PathConditions {
     assumption match {
       case quantification: Quantification => quantification.isGlobal
       case _: IsReadPermVar => true
+      case _: HasDomain => true
       case _ => false
     }
   }

Original file line number	Diff line number	Diff line change
`@@ -679,6 +679,7 @@ object PathConditions {`
`679`	`679`	`assumption match {`
`680`	`680`	`case quantification: Quantification => quantification.isGlobal`
`681`	`681`	`case _: IsReadPermVar => true`
	`682`	`+ case _: HasDomain => true`
`682`	`683`	`case _ => false`
`683`	`684`	`}`
`684`	`685`	`}`