Fix to Lheap_Add translation (#740)

Lheap_Add primitive adds a cell to a linear heap. This PR changes the
translation so that only the domain of the target heap is modified. The
heap contents is assumed (magically) to contain the value being inserted
at the fresh address. This is sound because Ref T, the address type for
Lheap T is uninterpreted and potentially infinite source of cells with a
particular value.

Source/Concurrency/LinearRewriter.cs

@@ -302,11 +302,12 @@ private List<Cmd> RewriteLheapAdd(CallCmd callCmd)
 
     cmdSeq.Add(CmdHelper.HavocCmd(k));
     cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Not(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Dom(path), k))));
+    cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Eq(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Val(path), k), v)));
     cmdSeq.Add(CmdHelper.AssignCmd(
       CmdHelper.ExprToAssignLhs(path),
       ExprHelper.FunctionCall(lheapConstructor,
         ExprHelper.FunctionCall(new MapStore(callCmd.tok, 1), Dom(path), k, Expr.True),
-        ExprHelper.FunctionCall(new MapStore(callCmd.tok, 1), Val(path), k, v))));
+        Val(path))));
 
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;