keep Old() when rewriting spec for param form to support memload/store (#364)

ailrst · web-flow · commit b1eb0868b85d · 2025-03-12T14:03:07.000+10:00
diff --git a/src/main/scala/ir/transforms/ProcedureParameters.scala b/src/main/scala/ir/transforms/ProcedureParameters.scala
@@ -570,7 +570,7 @@ def specToProcForm(
       case b: QuantifierExpr => b
       case b: Old => {
         if (isPost) {
-          convVarToOld(varInPre, varInPost, false)(b.body)
+          Old(convVarToOld(varInPre, varInPost, false)(b.body))
         } else {
           throw Exception("Illegal nested or non-relation Old()")
         }

Original file line number	Diff line number	Diff line change
`@@ -570,7 +570,7 @@ def specToProcForm(`
`570`	`570`	`case b: QuantifierExpr => b`
`571`	`571`	`case b: Old => {`
`572`	`572`	`if (isPost) {`
`573`		`- convVarToOld(varInPre, varInPost, false)(b.body)`
	`573`	`+ Old(convVarToOld(varInPre, varInPost, false)(b.body))`
`574`	`574`	`} else {`
`575`	`575`	`throw Exception("Illegal nested or non-relation Old()")`
`576`	`576`	`}`