xlang correctly handles short circuit with side effects

src/main/scala/leon/xlang/ImperativeCodeElimination.scala

@@ -252,6 +252,16 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
         }
         (i, scope, Map())
 
+      case And(args) => {
+        val ifExpr = args.reduceRight((el, acc) => IfExpr(el, acc, BooleanLiteral(false)))
+        toFunction(ifExpr)
+      }
+
+      case Or(args) => {
+        val ifExpr = args.reduceRight((el, acc) => IfExpr(el, BooleanLiteral(true), acc))
+        toFunction(ifExpr)
+      }
+
       case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
       case n @ NAryOperator(args, recons) => {
         val (recArgs, scope, fun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {

src/test/resources/regression/verification/xlang/valid/ShortCircuit.scala

+import leon.lang._
+import leon.collection._
+import leon._
+
+object ShortCircuit {
+
+  def negate(a: Boolean) = {
+    var b = true
+    a && { b = false; true }
+    b
+  } ensuring { res => res != a }
+
+  def negateOr(a: Boolean) = {
+    var b = false
+    a || { b = true; true }
+    b
+  } ensuring { res => res != a }
+
+}