diff --git a/Source/Dafny/Verifier/Translator.BoogieFactory.cs b/Source/Dafny/Verifier/Translator.BoogieFactory.cs
index 1bbb2c8cc5e..37ef4f11e6e 100644
--- a/Source/Dafny/Verifier/Translator.BoogieFactory.cs
+++ b/Source/Dafny/Verifier/Translator.BoogieFactory.cs
@@ -185,8 +185,15 @@ private static Bpl.Expr GetLit(Bpl.Expr expr) {
     }
 
     public static Bpl.AssumeCmd TrAssumeCmd(Bpl.IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes = null) {
-      var lit = RemoveLit(expr);
-      return attributes == null ? new Bpl.AssumeCmd(tok, lit) : new Bpl.AssumeCmd(tok, lit, attributes);
+      var litArgument = GetLit(expr);
+      if (litArgument is Bpl.LiteralExpr literalExpr && literalExpr.asBool) {
+        // In most cases, we leave any Lit brackets that "expr" may have. In the past, these brackets
+        // had always been removed here. Alas, some brittle test cases stopped verifying if we
+        // keep "assume Lit(true)" instead of simplifying it to "assume true". Therefore, as a
+        // special case, we remove the Lit brackets from the literal "true".
+        expr = litArgument;
+      }
+      return attributes == null ? new Bpl.AssumeCmd(tok, expr) : new Bpl.AssumeCmd(tok, expr, attributes);
     }
 
     static Bpl.Expr RemoveLit(Bpl.Expr expr) {
diff --git a/Source/Dafny/Verifier/Translator.cs b/Source/Dafny/Verifier/Translator.cs
index 28c7b02801b..2c817c7053e 100644
--- a/Source/Dafny/Verifier/Translator.cs
+++ b/Source/Dafny/Verifier/Translator.cs
@@ -10225,6 +10225,15 @@ Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)
       return Assert(tok, condition, errorMessage, tok);
     }
 
+    Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.QKeyValue kv) {
+      Contract.Requires(tok != null);
+      Contract.Requires(errorMessage != null);
+      Contract.Requires(condition != null);
+      Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
+
+      return Assert(tok, condition, errorMessage, tok, kv);
+    }
+
     Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.IToken refinesToken, Bpl.QKeyValue kv = null) {
       Contract.Requires(tok != null);
       Contract.Requires(condition != null);
@@ -10237,13 +10246,14 @@ Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage,
       } else {
         var cmd = TrAssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);
         cmd.ErrorData = "Error: " + errorMessage;
-        this.assertionCount++;
         return cmd;
       }
     }
+
     Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessage) {
       return AssertNS(tok, condition, errorMessage, tok, null);
     }
+
     Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.IToken refinesTok, Bpl.QKeyValue kv) {
       Contract.Requires(tok != null);
       Contract.Requires(errorMessage != null);
@@ -10263,22 +10273,6 @@ Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessag
       }
     }
 
-    Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.QKeyValue kv) {
-      Contract.Requires(tok != null);
-      Contract.Requires(errorMessage != null);
-      Contract.Requires(condition != null);
-      Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
-
-      if (assertAsAssume || (RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) {
-        // produce an assume instead
-        return TrAssumeCmd(tok, condition, kv);
-      } else {
-        var cmd = TrAssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);
-        cmd.ErrorData = "Error: " + errorMessage;
-        return cmd;
-      }
-    }
-
     Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessage, string comment) {
       Contract.Requires(tok != null);
       Contract.Requires(condition != null);
@@ -10707,8 +10701,13 @@ Expression Zero(IToken tok, Type typ) {
     delegate Bpl.Expr ExpressionConverter(Dictionary<IVariable, Expression> substMap, ExpressionTranslator etran);
 
     Bpl.AssertCmd TrAssertCmd(IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes = null) {
-      var lit = RemoveLit(expr);
-      return attributes == null ? new Bpl.AssertCmd(tok, lit) : new Bpl.AssertCmd(tok, lit, attributes);
+      // It may be that "expr" is a Lit expression. It might seem we don't need a Lit expression
+      // around the boolean expression that is being asserted. However, we keep it. For one,
+      // it doesn't change the semantics of the assert command. More importantly, leaving
+      // a Lit around the expression is useful to avoid sending an "assert false;" to Boogie--since
+      // Boogie looks especially for "assert false;" commands and processes them in such a way
+      // that loops no longer are loops (which is confusing for Dafny users).
+      return attributes == null ? new Bpl.AssertCmd(tok, expr) : new Bpl.AssertCmd(tok, expr, attributes);
     }
 
     delegate void BodyTranslator(BoogieStmtListBuilder builder, ExpressionTranslator etr);
diff --git a/Test/dafny0/NoMoreAssume2Less2.dfy b/Test/dafny0/NoMoreAssume2Less2.dfy
new file mode 100644
index 00000000000..a9da0ddd57b
--- /dev/null
+++ b/Test/dafny0/NoMoreAssume2Less2.dfy
@@ -0,0 +1,199 @@
+// RUN: %dafny "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file tests various ways of writing the equivalent of "assume false;" or "assert false;" inside a loop.
+// It used to be that Dafny's translation of such statements into Boogie could cause Boogie to cut off the
+// loop back edge, which would turn a loop into something that wasn't a loop. In particular, it would cause
+// the expected "havoc loop_targets;" statement never to be generated, whose dramatic impact on what gets
+// verified would be both mysterious and surprising to most Dafny users.
+//
+// The equally mysterious workaround for this problem used to be for Dafny users to replace their "assume false;"
+// with something like "assume 2 < 2;", which Boogie wouldn't recognize in the same way.
+//
+// The current translation to Boogie makes sure that no user-supplied expression turns into exactly an
+// "assume false;" or "assert false;". This means that Dafny users can use a statement like "assume false;"
+// without chopping off back edges.
+//
+// It is still possible (in situations that would be rare in practice) to get some initially-surprising behavior
+// from Boogie, because it is possible to introduce a "false" condition that will be detected by the control-flow
+// handling in Boogie's abstract interpreter. Method Conjuncts4 below shows such an example.
+
+method M0(n: nat) {
+  var i := 0;
+  while i < n {
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method M1(n: nat) {
+  var i := 0;
+  while i < n {
+    assume false;
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method M2(n: nat) {
+  var i := 0;
+  while i < n {
+    assume 2 < 2;
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method M3(n: nat) {
+  var i := 0;
+  while i < n {
+    assert false; // error
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method M4(n: nat) {
+  var i := 0;
+  while i < n {
+    assert 2 < 2; // error
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method M5(n: nat) {
+  var i := 0;
+  while i < n {
+    assert false by { // error
+    }
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+predicate P() { true }
+predicate Q() { true }
+predicate R(n: nat) { true }
+predicate False() { false }
+
+method Conjuncts0(n: nat) {
+  var i := 0;
+  while i < n {
+    assume P() && false && Q();
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method Conjuncts1(n: nat) {
+  var i := 0;
+  while i < n {
+    assert P() && false && Q(); // error
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method Conjuncts2(n: nat) {
+  var i := 0;
+  while i < n {
+    assume False();
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method Conjuncts3(n: nat) {
+  var i := 0;
+  while i < n {
+    assert False(); // error
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method Conjuncts4(n: nat, m: nat) {
+  var i := 0;
+  while i < n {
+    assert R(m) && false; // error
+    i := i + 1;
+  }
+  // The following assertion is provable, because the "false" in the assertion above
+  // gets noticed by Boogie's abstract interpreter, which then (correctly) figures out
+  // that no control leads from inside the loop back to the loop head. Therefore, it
+  // infers the loop invariant i == 0.
+  // It takes a special (and unusual) condition to get this behavior. This example
+  // uses two conjuncts, one of which is "false" and one of which is a non-Lit expression.
+  assert n == 0;
+}
+
+method LoopInvariants(n: nat) {
+  var i := 0;
+  while i < n {
+    for j := 0 to 5
+      invariant false // error
+    {
+    }
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method Calls0(n: nat) {
+  var i := 0;
+  while i < n {
+    FalsePre(); // error
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method Calls1(n: nat) {
+  var i := 0;
+  while i < n {
+    FalsePost();
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method FalsePre()
+  requires false
+
+method FalsePost()
+  ensures false
+
+method LabeledExpressions0(n: nat)
+  requires A: false
+{
+  var i := 0;
+  while i < n {
+    reveal A;
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method LabeledExpressions1(n: nat)
+{
+  assert A: false; // error
+  var i := 0;
+  while i < n {
+    reveal A;
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
+
+method LabeledExpressions2(n: nat)
+{
+  assert A: false by { // error
+  }
+  var i := 0;
+  while i < n {
+    reveal A;
+    i := i + 1;
+  }
+  assert n == 0; // error
+}
diff --git a/Test/dafny0/NoMoreAssume2Less2.dfy.expect b/Test/dafny0/NoMoreAssume2Less2.dfy.expect
new file mode 100644
index 00000000000..5b33944793d
--- /dev/null
+++ b/Test/dafny0/NoMoreAssume2Less2.dfy.expect
@@ -0,0 +1,31 @@
+NoMoreAssume2Less2.dfy(26,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(35,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(44,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(50,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(53,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(59,13): Error: assertion violation
+NoMoreAssume2Less2.dfy(62,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(68,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(72,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(86,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(92,18): Error: assertion violation
+NoMoreAssume2Less2.dfy(95,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(104,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(110,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(78,20): Related location
+NoMoreAssume2Less2.dfy(113,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(119,19): Error: assertion violation
+NoMoreAssume2Less2.dfy(135,16): Error: This loop invariant might not hold on entry.
+NoMoreAssume2Less2.dfy(135,16): Related message: loop invariant violation
+NoMoreAssume2Less2.dfy(140,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(146,12): Error: A precondition for this call might not hold.
+NoMoreAssume2Less2.dfy(162,11): Related location: This is the precondition that might not hold.
+NoMoreAssume2Less2.dfy(149,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(158,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(175,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(180,12): Error: assertion violation
+NoMoreAssume2Less2.dfy(186,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(191,12): Error: assertion violation
+NoMoreAssume2Less2.dfy(198,11): Error: assertion violation
+
+Dafny program verifier finished with 0 verified, 26 errors
diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
index 8feed44cc69..30a1453137e 100644
--- a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
@@ -1,6 +1,6 @@
 Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> DoNothingToAssert
-Processing command (at Snapshots0.v0.dfy(4,10)) assert false;
+Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors
@@ -11,7 +11,7 @@ Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f
   >>> MarkAsFullyVerified
 Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
   >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots0.v1.dfy(4,10)) assert false;
+Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);
   >>> MarkAsPartiallyVerified
 Snapshots0.v1.dfy(4,9): Error: assertion violation
 
diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
index dab415ec196..9e398999d11 100644
--- a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
@@ -1,6 +1,6 @@
 Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> DoNothingToAssert
-Processing command (at Snapshots1.v0.dfy(4,10)) assert false;
+Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors
@@ -8,7 +8,7 @@ Processing call to procedure Call$$_module.__default.N in implementation Impl$$_
   >>> added after: a##cached##0 := a##cached##0 && false;
 Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> MarkAsFullyVerified
-Processing command (at Snapshots1.v1.dfy(4,10)) assert false;
+Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);
   >>> DoNothingToAssert
 Snapshots1.v1.dfy(4,9): Error: assertion violation
 
diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
index 18f5a65e958..d188c579d57 100644
--- a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
@@ -1,6 +1,6 @@
 Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(4,10)) assert false;
+Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
   >>> DoNothingToAssert
 Processing command (at Snapshots2.v0.dfy(11,11)) assert true;
   >>> DoNothingToAssert
@@ -20,7 +20,7 @@ Processing implementation CheckWellformed$$_module.__default.Q (at Snapshots2.v1
   >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
 Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(4,10)) assert false;
+Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);
   >>> DoNothingToAssert
 Snapshots2.v1.dfy(4,9): Error: assertion violation
 Processing command (at Snapshots2.v1.dfy(11,11)) assert true;
diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
index cc8f47b4786..252532fada2 100644
--- a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
@@ -1,11 +1,11 @@
-Processing command (at Snapshots3.v0.dfy(9,14)) assert 0 != 0;
+Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0);
   >>> DoNothingToAssert
 Snapshots3.v0.dfy(9,13): Error: assertion violation
 
 Dafny program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots3.v1.dfy(5,12)) assert true;
+Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots3.v1.dfy(9,14)) assert 0 != 0;
+Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0);
   >>> RecycleError
 Snapshots3.v0.dfy(9,13): Error: assertion violation
 
diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
index fd0a91d285f..8f7568134db 100644
--- a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
@@ -2,11 +2,11 @@ Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0);
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots4.v1.dfy(5,14)) assert 1 != 1;
+Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1);
   >>> DoNothingToAssert
 Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0);
   >>> MarkAsFullyVerified
-Processing command (at Snapshots4.v1.dfy(10,14)) assert 2 != 2;
+Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2);
   >>> DoNothingToAssert
 Snapshots4.v1.dfy(5,13): Error: assertion violation
 Snapshots4.v1.dfy(10,13): Error: assertion violation
diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect
index 808125eddb6..e4dfe388410 100644
--- a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect
@@ -16,7 +16,7 @@ Snapshots8.v0.dfy(13,12): Related location: This is the postcondition that might
 Processing command (at Snapshots8.v0.dfy(23,12)) assert u#0 != 53;
   >>> DoNothingToAssert
 Snapshots8.v0.dfy(23,11): Error: assertion violation
-Processing command (at Snapshots8.v0.dfy(28,10)) assert true;
+Processing command (at Snapshots8.v0.dfy(28,10)) assert Lit(true);
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 4 errors
@@ -37,7 +37,7 @@ Snapshots8.v1.dfy(5,16): Error: assertion violation
 Snapshots8.v1.dfy(6,7): Error: A precondition for this call might not hold.
 Snapshots8.v1.dfy(12,20): Related location: This is the precondition that might not hold.
 Snapshots8.v1.dfy(7,11): Error: assertion violation
-Processing command (at Snapshots8.v1.dfy(23,12)) assert true;
+Processing command (at Snapshots8.v1.dfy(23,12)) assert Lit(true);
   >>> DoNothingToAssert
 Processing command (at Snapshots8.v1.dfy(19,13)) assert LitInt(2) <= z#0;
   >>> DoNothingToAssert