[fix] Use local variables for assume statements (#870)

Author: Ang9876

Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs

@@ -569,6 +569,8 @@ private void EmitLine(string str)
     private static string StateAdtReceivedSelector => $"{StateAdt}_Received";
     private static string StateAdtMachinesSelector => $"{StateAdt}_Machines";
 
+    private static bool useLocalPrefix = false;
+
     private static string StateAdtConstruct(string sent, string received, string machines)
     {
         return
@@ -598,7 +600,7 @@ private static string StateAdtDeclaration()
 
     private static string InFlight(string state, string action)
     {
-        return $"({StateAdtSelectSent(state)}[{action}] && !{StateAdtSelectReceived(state)}[{action}])";
+        return useLocalPrefix ? $"({LocalPrefix}sent[{action}] && !{StateAdtSelectReceived(state)}[{action}])" : $"({StateAdtSelectSent(state)}[{action}] && !{StateAdtSelectReceived(state)}[{action}])";
     }
 
     private static string StateVar => $"{BuiltinPrefix}State";
@@ -1024,7 +1026,9 @@ private void GenerateSpecProcedures(List<Machine> specs, List<Invariant> goals,
                 foreach (var v in spec.Fields)
                     EmitLine($"{GetLocalName(v)} = {SpecPrefix}{spec.Name}_{v.Name};");
 
+                useLocalPrefix = true;
                 GenerateStmt(f.Body, spec, goals, generateSanityChecks);
+                useLocalPrefix = false;
 
                 // update the global variables
                 EmitLine($"{SpecPrefix}{spec.Name}_State = {LocalPrefix}state;");
@@ -1406,7 +1410,9 @@ private void GenerateMachineProcedures(Machine m, List<Invariant> goals, bool ge
                 EmitLine($"{GetLocalName(v)} = {MachineStateAdtSelectField(currState, m, v)};");
             // foreach (var v in f.LocalVariables) EmitLine($"{GetLocalName(v)} = {DefaultValue(v.Type)};");
 
+            useLocalPrefix = true;
             GenerateStmt(f.Body, null, goals, generateSanityChecks);
+            useLocalPrefix = false;
 
             var fields = m.Fields.Select(GetLocalName).Prepend($"{LocalPrefix}state").ToList();
 
@@ -2042,7 +2048,7 @@ ContainsExpr cexp when cexp.Collection.Type.Canonicalize() is SetType =>
                 s), // must deref for ADT!
             PureCallExpr pexpr => $"{pexpr.Pure.Name}({string.Join(", ", pexpr.Arguments.Select(ExprToString))})",
             FlyingExpr fexpr => $"{InFlight(StateVar, ExprToString(fexpr.Instance))}",
-            SentExpr sexpr => $"{StateAdtSelectSent(StateVar)}[{ExprToString(sexpr.Instance)}]",
+            SentExpr sexpr => useLocalPrefix ? $"{LocalPrefix}sent[{ExprToString(sexpr.Instance)}]" : $"{StateAdtSelectSent(StateVar)}[{ExprToString(sexpr.Instance)}]",
             TargetsExpr texpr =>
                 $"({LabelAdtSelectTarget(ExprToString(texpr.Instance))} == {ExprToString(texpr.Target)})",
             _ => throw new NotSupportedException($"Not supported expr ({expr}) at {GetLocation(expr)}")