diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 57929b71d..ae427d057 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1287,7 +1287,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { codomainQVars, relevantChunks, v1, - optSmDomainDefinitionCondition = if (s2.smDomainNeeded) Some(True) else None, + optSmDomainDefinitionCondition = None, optQVarsInstantiations = Some(arguments)) val permsTaken = result match { case Complete() => rPerm @@ -1332,7 +1332,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource = resource, codomainQVars = codomainQVars, relevantChunks = relevantChunks, - optSmDomainDefinitionCondition = if (s1.smDomainNeeded) Some(True) else None, + optSmDomainDefinitionCondition = None, optQVarsInstantiations = Some(arguments), v = v) val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1), diff --git a/src/main/scala/state/SnapshotMapCache.scala b/src/main/scala/state/SnapshotMapCache.scala index 5a7f313ee..5672e453b 100644 --- a/src/main/scala/state/SnapshotMapCache.scala +++ b/src/main/scala/state/SnapshotMapCache.scala @@ -46,7 +46,10 @@ case class SnapshotMapCache private ( : Option[SnapshotMapCache.Value] = { cache.get(key) match { - case Some((smDef, totalPermissions, `optSmDomainDefinitionCondition`)) => + case Some((smDef, totalPermissions, cachedSmDomainDefinitionCondition)) + if cachedSmDomainDefinitionCondition == optSmDomainDefinitionCondition || // defined under the same condition + (cachedSmDomainDefinitionCondition.contains(terms.True) && optSmDomainDefinitionCondition.isEmpty) // cached is always defined and we don't need a domain + => Some((smDef, totalPermissions)) case _ =>