[Civl] Enhance quantifier elimination (#829)

TryElimination looks for a substitution for the lhs of single-static
assignments on a path-by-path basis through an atomic action. If an
assignment is of the form ```x := v``` where both x and v are variables,
it is possible that x is defined but v is not. In such a case, the code
change interprets the assignment as an equality and infers a definition
```v <-- x```.

Source/Concurrency/TransitionRelationComputation.cs

@@ -374,6 +374,11 @@ private void TryElimination(IEnumerable<Variable> extraDefinedVariables)
               varToExpr[assignment.Var] = SubstitutionHelper.Apply(varToExpr, assignment.Expr);
               changed = true;
             }
+            else if (Defined(assignment.Var) && assignment.Expr is IdentifierExpr ie && !Defined(ie.Decl))
+            {
+              varToExpr[ie.Decl] = SubstitutionHelper.Apply(varToExpr, Expr.Ident(assignment.Var));
+              changed = true;
+            }
             else
             {
               remainingAssignments.Add(assignment);

Test/civl/regression-tests/qelim1.bpl

@@ -0,0 +1,14 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+atomic action {:layer 2} AtomicFoo() returns (o: int)
+{
+    var y: int;
+    o := y;
+}
+yield procedure {:layer 1} Foo() returns (o: int) 
+refines AtomicFoo;
+{
+    var x: int;
+    o := x;
+}

Test/civl/regression-tests/qelim1.bpl.expect

@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors