diff --git a/Source/Concurrency/TransitionRelationComputation.cs b/Source/Concurrency/TransitionRelationComputation.cs
index 46faf0eb8..6f760241e 100644
--- a/Source/Concurrency/TransitionRelationComputation.cs
+++ b/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);
diff --git a/Test/civl/regression-tests/qelim1.bpl b/Test/civl/regression-tests/qelim1.bpl
new file mode 100644
index 000000000..739dc5c19
--- /dev/null
+++ b/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;
+}
\ No newline at end of file
diff --git a/Test/civl/regression-tests/qelim1.bpl.expect b/Test/civl/regression-tests/qelim1.bpl.expect
new file mode 100644
index 000000000..37fad75c9
--- /dev/null
+++ b/Test/civl/regression-tests/qelim1.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors