diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs index 22b17815d15..c51b107f6d4 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs @@ -370,7 +370,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn } TrAssignSuchThat(new List(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], - e.Constraint_Bounds, e.tok.line, w, inLetExprBody); + e.Constraint_Bounds, w, inLetExprBody); EmitReturnExpr(e.Body, e.Body.Type, true, w); } } diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs index b51afc2021e..ecce27f2eea 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs @@ -158,7 +158,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree } } else { Contract.Assert(s.Bounds != null); - TrAssignSuchThat(lhss, s.Expr, s.Bounds, s.Tok.line, wr, false); + TrAssignSuchThat(lhss, s.Expr, s.Bounds, wr, false); } break; diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index d807b4a42fa..c4069d85ac9 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -3538,7 +3538,7 @@ private void IntroduceAndAssignBoundVars(ExistsExpr exists, ConcreteSyntaxTree w TrLocalVar(bv, false, wr); } var ivars = exists.BoundVars.ConvertAll(bv => (IVariable)bv); - TrAssignSuchThat(ivars, exists.Term, exists.Bounds, exists.tok.line, wr, false); + TrAssignSuchThat(ivars, exists.Term, exists.Bounds, wr, false); } private bool CanSequentializeForall(List bvs, List bounds, Expression range, Expression lhs, Expression rhs) { @@ -3665,7 +3665,7 @@ protected override bool VisitOneExpr(Expression expr, ref object st) { } } - private void TrAssignSuchThat(List lhss, Expression constraint, List bounds, int debuginfoLine, ConcreteSyntaxTree wr, bool inLetExprBody) { + private void TrAssignSuchThat(List lhss, Expression constraint, List bounds, ConcreteSyntaxTree wr, bool inLetExprBody) { Contract.Requires(lhss != null); Contract.Requires(constraint != null); Contract.Requires(bounds != null); @@ -3741,7 +3741,7 @@ private void TrAssignSuchThat(List lhss, Expression constraint, List< copyInstrWriters.Pop(); // Java compiler throws unreachable error when absurd statement is written after unbounded for-loop, so we don't write it then. - EmitAbsurd(string.Format("assign-such-that search produced no value (line {0})", debuginfoLine), wrOuter, needIterLimit); + EmitAbsurd("assign-such-that search produced no value", wrOuter, needIterLimit); } protected interface ILvalue { diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index a5f1af719e7..8ff0b871599 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -5691,7 +5691,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv goto after__ASSIGN_SUCH_THAT_0; } } - throw new System.Exception("assign-such-that search produced no value (line 4771)"); + throw new System.Exception("assign-such-that search produced no value"); after__ASSIGN_SUCH_THAT_0: ; _63_allReadCloned = Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(_63_allReadCloned, Dafny.Sequence.UnicodeFromString("let ")), _64_next), Dafny.Sequence.UnicodeFromString(" = ")), _64_next), Dafny.Sequence.UnicodeFromString(".clone();\n")); _62_recIdents = Dafny.Set>.Difference(_62_recIdents, Dafny.Set>.FromElements(_64_next)); @@ -7047,7 +7047,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv goto after__ASSIGN_SUCH_THAT_1; } } - throw new System.Exception("assign-such-that search produced no value (line 5307)"); + throw new System.Exception("assign-such-that search produced no value"); after__ASSIGN_SUCH_THAT_1: ; if ((!object.Equals(selfIdent, DCOMP.SelfInfo.create_NoSelf())) && ((_310_next).Equals(Dafny.Sequence.UnicodeFromString("_this")))) { RAST._IExpr _311_selfCloned; diff --git a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs index 8948704f25e..f3fa77fd41f 100644 --- a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs +++ b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs @@ -46,7 +46,7 @@ public static __T UniqueElementOf<__T>(Dafny.ISet<__T> s) { goto after__ASSIGN_SUCH_THAT_0; } } - throw new System.Exception("assign-such-that search produced no value (line 105)"); + throw new System.Exception("assign-such-that search produced no value"); after__ASSIGN_SUCH_THAT_0: ; return _0_e; } diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs index 8f4194df420..14dfd647ee3 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs @@ -364,7 +364,7 @@ public static Dafny.ISequence<__T> SetToSeq<__T>(Dafny.ISet<__T> s) goto after__ASSIGN_SUCH_THAT_0; } } - throw new System.Exception("assign-such-that search produced no value (line 7245)"); + throw new System.Exception("assign-such-that search produced no value"); after__ASSIGN_SUCH_THAT_0: ; _0_left = Dafny.Set<__T>.Difference(_0_left, Dafny.Set<__T>.FromElements(_1_x)); xs = Dafny.Sequence<__T>.Concat(xs, Dafny.Sequence<__T>.FromElements(_1_x));