diff --git a/Source/Dafny/Compilers/Compiler.cs b/Source/Dafny/Compilers/Compiler.cs index 284e8da3510..4b3baf32893 100644 --- a/Source/Dafny/Compilers/Compiler.cs +++ b/Source/Dafny/Compilers/Compiler.cs @@ -415,7 +415,7 @@ protected virtual void EmitMultiAssignment(List lhsExprs, List w.Write(target), resolved.Obj.Type, resolved.Member, typeArgs, resolved.TypeArgumentSubstitutionsWithParents(), resolved.Type); + ILvalue newLhs = EmitMemberSelect(w => w.Write(target), resolved.Obj.Type, resolved.Member, typeArgs, resolved.TypeArgumentSubstitutionsWithParents(), resolved.Type, internalAccess: enclosingMethod is Constructor); lhssn.Add(newLhs); } else if (lexpr is SeqSelectExpr) { var seqExpr = (SeqSelectExpr)lexpr; @@ -5149,4 +5149,4 @@ public void WriteLegendFile() { } } } -} +} \ No newline at end of file diff --git a/Test/git-issues/git-issue-1111.dfy b/Test/git-issues/git-issue-1111.dfy index 2ff968d2a4b..b602d34b5f2 100644 --- a/Test/git-issues/git-issue-1111.dfy +++ b/Test/git-issues/git-issue-1111.dfy @@ -15,31 +15,4 @@ module Foo { { var o := new A(1, 2); } -} - -/* -public class A { - public A() { - this._a = java.math.BigInteger.ZERO; - this._b = java.math.BigInteger.ZERO; - } - public void __ctor(java.math.BigInteger k, java.math.BigInteger j) - { - (this)._a = k; - (this)._b = j; - } - public java.math.BigInteger _a; - public java.math.BigInteger a() - { - return this._a; - } - public java.math.BigInteger _b; - public java.math.BigInteger b() - { - return this._b; - } - private static final dafny.TypeDescriptor _TYPE = dafny.TypeDescriptor.referenceWithInitializer(A.class, () -> (A) null); - public static dafny.TypeDescriptor _typeDescriptor() { - return (dafny.TypeDescriptor) (dafny.TypeDescriptor) _TYPE; - } -*/ \ No newline at end of file +} \ No newline at end of file