Replace old expressions in all assert and assume in the method

Author: tornado80

src/lib.rs

@@ -638,9 +638,9 @@ fn cmd_to_ivlcmd(cmd: &Cmd, method_context: &MethodContext, loop_context: &LoopC
     let &Cmd { kind, span, .. } = &cmd;
     Ok(match kind {
         CmdKind::Assert { condition, message } =>
-            IVLCmd::assert(condition, message),
+            IVLCmd::assert(&replace_old_in_expression(condition, &method_context.global_variables_old_values), message),
         CmdKind::Assume { condition} =>
-            IVLCmd::assume(condition),
+            IVLCmd::assume(&replace_old_in_expression(condition, &method_context.global_variables_old_values)),
         CmdKind::Seq(cmd1, cmd2) =>
             cmd_to_ivlcmd(cmd1, &method_context, loop_context)?.seq(
                 &cmd_to_ivlcmd(cmd2, &method_context, loop_context)?),

tests/global-replace-old-in-body-bad.slang

@@ -0,0 +1,10 @@
+global x: Int := 2
+
+method c()
+modifies x
+
+{
+    x := x + 1;
+    // @CheckError
+    assert x == old(x) + 2
+}

tests/global-replace-old-in-body-good.slang

@@ -0,0 +1,9 @@
+global x: Int := 2
+
+method c()
+modifies x
+
+{
+    x := x + 1;
+    assert x == old(x) + 1
+}