diff --git a/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala b/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
new file mode 100644
index 000000000..049e37dec
--- /dev/null
+++ b/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
@@ -0,0 +1,337 @@
+package viper.silver.ast.utility
+
+import viper.silver.ast._
+import viper.silver.ast.utility.Statements.EmptyStmt
+import viper.silver.utility.Common.Rational
+
+import scala.collection.mutable
+import scala.collection.mutable._
+
+trait IterativeSimplifier {
+
+  /**
+   * Simplify 'n' by matching nodes in the AST with a list of transformations
+   * while storing every version of n generated and applying simplify to the stored
+   * versions until no new versions are generated or the number of versions is greater than
+   * iterationLimit
+   */
+  def simplify[N <: Node](n: N, assumeWelldefinedness: Boolean = false, iterationLimit: Integer = 5000, printToConsole: Boolean = false): N = {
+
+    val visited: ArrayBuffer[N] = ArrayBuffer(n)
+    val queue: mutable.Queue[N] = mutable.Queue(n)
+
+    while (queue.nonEmpty && visited.length < iterationLimit) {
+      val currnode: N = queue.dequeue()
+      if(printToConsole) {
+        println("currnode: " + currnode)
+      }
+
+      val generated: ArrayBuffer[N] = pfRecSimplify(currnode, assumeWelldefinedness)
+      if(printToConsole) {
+        println("generated: " + generated)
+      }
+      for (g <- generated if !visited.contains(g)) {
+        visited.append(g)
+        queue.enqueue(g)
+      }
+    }
+
+    if(printToConsole){
+      println("result simplify: " + visited)
+    }
+
+    getShortest(visited)
+  }
+
+  protected def getShortest[N <: Node](visited: ArrayBuffer[N]): N = {
+    visited.minBy(treeSize)
+  }
+
+  // "counts every node twice", ie "LocalVar("a", Bool)()" is counted once as "a" and once as "Bool"
+  private def treeSize[N <: Node](n: N): Int = {
+    n.reduceTree[Int]((node, count) => (count.sum + 1))
+  }
+  private def treeHasDoubleNeg[N <: Node](n: N): Boolean = {
+    n.reduceTree[Boolean]((node, doubleNegs) => doubleNegs.contains(true) || isDoubleNeg(node))
+  }
+
+  def pfSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
+
+    val result: ArrayBuffer[N] = ArrayBuffer()
+
+    result ++= pfSilverCases(n, assumeWelldefinedness)
+
+    result
+  }
+
+  protected def pfSilverCases[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
+    val result: ArrayBuffer[Node] = ArrayBuffer()
+
+    val cases: List[PartialFunction[N, Node]] = List(
+      { case root@Not(BoolLit(literal)) => BoolLit(!literal)(root.pos, root.info) },
+
+      { case root@Not(EqCmp(a, b)) => NeCmp(a, b)(root.pos, root.info) },
+      { case root@Not(NeCmp(a, b)) => EqCmp(a, b)(root.pos, root.info) },
+      { case root@Not(GtCmp(a, b)) => LeCmp(a, b)(root.pos, root.info) },
+      { case root@Not(GeCmp(a, b)) => LtCmp(a, b)(root.pos, root.info) },
+      { case root@Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info) },
+      { case root@Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info) },
+
+      { case Not(Not(single)) => single },
+
+      { case Or(FalseLit(), right) => right },
+      { case Or(left, FalseLit()) => left },
+      { case root@Or(TrueLit(), _) => TrueLit()(root.pos, root.info) },
+      { case root@Or(_, TrueLit()) => TrueLit()(root.pos, root.info) },
+
+      { case And(TrueLit(), right) => right },
+      { case And(left, TrueLit()) => left },
+      { case root@And(FalseLit(), _) => FalseLit()(root.pos, root.info) },
+      { case root@And(_, FalseLit()) => FalseLit()(root.pos, root.info) },
+
+      //Idempotence
+      { case root@And(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) && a == b => a},
+      { case root@Or(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) && a == b => a},
+
+      { case root@And(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) => And(b, a)(root.pos, root.info)},
+      { case root@Or(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) => Or(b, a)(root.pos, root.info)},
+
+      { case root@And(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) => And(b, a)(root.pos, root.info)},
+      { case root@Or(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) => Or(b, a)(root.pos, root.info)},
+
+
+      //associativity
+      { case root@And(And(left, right), rchild) => And(left, And(right, rchild)(root.pos, root.info))(root.pos, root.info)},
+      { case root@And(lchild, And(left, right)) => And(And(lchild, left)(root.pos, root.info), right)(root.pos, root.info)},
+
+      { case root@Or(Or(left, right), uright) => Or(left, Or(right, uright)(root.pos, root.info))(root.pos, root.info)},
+      { case root@Or(uleft, Or(left, right)) => Or(Or(uleft, left)(root.pos, root.info), right)(root.pos, root.info)},
+
+      //implication rules
+      { case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info) },
+      { case Implies(TrueLit(), consequent) => consequent },
+      { case root@Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(root.pos, root.info), r)(root.pos, root.info) },
+
+      { case And(Implies(l1, r1), Implies(Not(l2), r2)) if assumeWelldefinedness && (l1 == l2 && r1 == r2) => r1 },
+
+      { case root@And(Implies(a, b), Implies(a2, c)) if a == a2 => Implies(a, And(b, c)(root.pos, root.info))(root.pos, root.info) },
+      { case And(Implies(a, b), Implies(Not(a2), b2)) if assumeWelldefinedness && a == a2 && b == b2 => b },
+      { case root@And(a, Implies(a2, b)) if a == a2 => And(a, b)(root.pos, root.info) },
+
+      //contrapositive
+      { case root@Implies(Not(left), Not(right)) if (assumeWelldefinedness || (left.isPure && right.isPure)) => Implies(right, left)(root.pos, root.info) },
+
+      //de morgan
+      { case root@Not(Or(left, right)) => And(Not(left)(), Not(right)())(root.pos, root.info)},
+      { case root@And(Not(left), Not(right)) => Not(Or(left, right)())(root.pos, root.info)},
+
+      { case root@Not(And(left, right)) => Or(Not(left)(), Not(right)())(root.pos, root.info)},
+      { case root@Or(Not(left), Not(right)) => Not(And(left, right)())(root.pos, root.info)},
+
+      //equality comparison
+
+      { case root@EqCmp(left, right) if assumeWelldefinedness && left == right => TrueLit()(root.pos, root.info) },
+      { case root@EqCmp(BoolLit(left), BoolLit(right)) => BoolLit(left == right)(root.pos, root.info) },
+      { case root@EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info) },
+      { case root@EqCmp(left, FalseLit()) => Not(left)(root.pos, root.info) },
+      { case EqCmp(TrueLit(), right) => right },
+      { case EqCmp(left, TrueLit()) => left },
+      { case root@EqCmp(IntLit(left), IntLit(right)) => BoolLit(left == right)(root.pos, root.info) },
+      { case root@EqCmp(NullLit(), NullLit()) => TrueLit()(root.pos, root.info) },
+
+      //nonequality comparison
+
+      { case root@NeCmp(BoolLit(left), BoolLit(right)) => BoolLit(left != right)(root.pos, root.info) },
+      { case NeCmp(FalseLit(), right) => right },
+      { case NeCmp(left, FalseLit()) => left },
+      { case root@NeCmp(TrueLit(), right) => Not(right)(root.pos, root.info) },
+      { case root@NeCmp(left, TrueLit()) => Not(left)(root.pos, root.info) },
+      { case root@NeCmp(IntLit(left), IntLit(right)) => BoolLit(left != right)(root.pos, root.info) },
+      { case root@NeCmp(NullLit(), NullLit()) => FalseLit()(root.pos, root.info) },
+      { case root@NeCmp(left, right) if assumeWelldefinedness && left == right => FalseLit()(root.pos, root.info) },
+
+      //extended equality/nonequality comparison
+      { case root@EqCmp(left, right) => EqCmp(right, left)(root.pos, root.info) },
+      { case root@NeCmp(left, right) => NeCmp(right, left)(root.pos, root.info) },
+      { case root@Not(EqCmp(left, right)) => NeCmp(left, right)(root.pos, root.info) },
+      { case root@Not(NeCmp(left, right)) => EqCmp(left, right)(root.pos, root.info) },
+      { case root@And(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => FalseLit()(root.pos, root.info)},
+      { case root@Or(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => TrueLit()(root.pos, root.info)},
+
+      //conditional expressions
+      { case CondExp(TrueLit(), ifTrue, _) => ifTrue },
+      { case CondExp(FalseLit(), _, ifFalse) => ifFalse },
+      { case CondExp(_, ifTrue, ifFalse) if assumeWelldefinedness && ifTrue == ifFalse => ifTrue },
+      { case root@CondExp(condition, FalseLit(), TrueLit()) => Not(condition)(root.pos, root.info) },
+      { case CondExp(condition, TrueLit(), FalseLit()) => condition },
+      { case root@CondExp(condition, FalseLit(), ifFalse) => And(Not(condition)(), ifFalse)(root.pos, root.info) },
+      { case root@CondExp(condition, TrueLit(), ifFalse) =>
+        if (ifFalse.isPure) {
+          Or(condition, ifFalse)(root.pos, root.info)
+        } else {
+          Implies(Not(condition)(), ifFalse)(root.pos, root.info)
+        }
+      },
+      { case root@CondExp(condition, ifTrue, FalseLit()) => And(condition, ifTrue)(root.pos, root.info) },
+      { case root@CondExp(condition, ifTrue, TrueLit()) => Implies(condition, ifTrue)(root.pos, root.info) },
+
+      //forall&exists
+      { case root@Forall(_, _, BoolLit(literal)) =>
+        BoolLit(literal)(root.pos, root.info) },
+      { case root@Exists(_, _, BoolLit(literal)) =>
+        BoolLit(literal)(root.pos, root.info) },
+
+      { case root@Minus(IntLit(literal)) => IntLit(-literal)(root.pos, root.info) },
+      { case Minus(Minus(single)) => single },
+
+      { case PermMinus(PermMinus(single)) => single },
+      { case PermMul(fst, FullPerm()) => fst },
+      { case PermMul(FullPerm(), snd) => snd },
+      { case root@PermMul(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val product = Rational(a, b) * Rational(c, d)
+        FractionalPerm(IntLit(product.numerator)(root.pos, root.info), IntLit(product.denominator)(root.pos, root.info))(root.pos, root.info)
+      case PermMul(_, np@NoPerm()) if assumeWelldefinedness => np
+      case PermMul(np@NoPerm(), _) if assumeWelldefinedness => np },
+
+
+      { case PermMul(wc@WildcardPerm(), _) if assumeWelldefinedness => wc },
+      { case PermMul(_, wc@WildcardPerm()) if assumeWelldefinedness => wc },
+
+      { case root@PermGeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info) },
+      { case root@PermLeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info) },
+      { case root@PermGtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info) },
+      { case root@PermLtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info) },
+
+      { case root@PermGtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) > Rational(c, d))(root.pos, root.info) },
+      { case root@PermGeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) >= Rational(c, d))(root.pos, root.info) },
+      { case root@PermLtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) < Rational(c, d))(root.pos, root.info) },
+      { case root@PermLeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) <= Rational(c, d))(root.pos, root.info) },
+      { case root@EqCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) == Rational(c, d))(root.pos, root.info) },
+      { case root@NeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) != Rational(c, d))(root.pos, root.info) },
+
+      { case root@PermLeCmp(NoPerm(), WildcardPerm()) =>
+        TrueLit()(root.pos, root.info) },
+      { case root@NeCmp(WildcardPerm(), NoPerm()) =>
+        TrueLit()(root.pos, root.info) },
+
+      { case DebugPermMin(e0@AnyPermLiteral(a, b), e1@AnyPermLiteral(c, d)) =>
+        if (Rational(a, b) < Rational(c, d)) {
+          e0
+        } else {
+          e1
+        }
+      },
+
+      { case root@PermSub(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val diff = Rational(a, b) - Rational(c, d)
+        FractionalPerm(IntLit(diff.numerator)(root.pos, root.info), IntLit(diff.denominator)(root.pos, root.info))(root.pos, root.info) },
+      { case root@PermAdd(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val sum = Rational(a, b) + Rational(c, d)
+        FractionalPerm(IntLit(sum.numerator)(root.pos, root.info), IntLit(sum.denominator)(root.pos, root.info))(root.pos, root.info) },
+      { case PermAdd(NoPerm(), rhs) => rhs },
+      { case PermAdd(lhs, NoPerm()) => lhs },
+      { case PermSub(lhs, NoPerm()) => lhs },
+
+      { case root@GeCmp(IntLit(left), IntLit(right)) =>
+        BoolLit(left >= right)(root.pos, root.info) },
+      { case root@GtCmp(IntLit(left), IntLit(right)) =>
+        BoolLit(left > right)(root.pos, root.info) },
+      { case root@LeCmp(IntLit(left), IntLit(right)) =>
+        BoolLit(left <= right)(root.pos, root.info) },
+      { case root@LtCmp(IntLit(left), IntLit(right)) =>
+        BoolLit(left < right)(root.pos, root.info) },
+
+      { case root@Add(IntLit(left), IntLit(right)) =>
+        IntLit(left + right)(root.pos, root.info) },
+      { case root@Sub(IntLit(left), IntLit(right)) =>
+        IntLit(left - right)(root.pos, root.info) },
+      { case root@Mul(IntLit(left), IntLit(right)) =>
+        IntLit(left * right)(root.pos, root.info) },
+      /* In the general case, Viper uses the SMT division and modulo. Scala's division is not in-sync with SMT division.
+         For nonnegative dividends and divisors, all used division and modulo definitions coincide. So, in order to not
+         not make any assumptions on the SMT division, division and modulo are simplified only if the dividend and divisor
+         are nonnegative. Also see Carbon PR #448.
+       */
+      { case root@Div(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+        IntLit(left / right)(root.pos, root.info) },
+      { case root@Mod(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+        IntLit(left % right)(root.pos, root.info) },
+
+      // statement simplifications
+      { case Seqn(EmptyStmt, _) => EmptyStmt }, // remove empty Seqn (including unnecessary scopedDecls)
+      { case s@Seqn(ss, scopedDecls) if ss.contains(EmptyStmt) => // remove empty statements
+        val newSS = ss.filterNot(_ == EmptyStmt)
+        Seqn(newSS, scopedDecls)(s.pos, s.info, s.errT) },
+      { case If(_, EmptyStmt, EmptyStmt) => EmptyStmt }, // remove empty If clause
+      { case If(TrueLit(), thn, _) => thn }, // remove trivial If conditions
+      { case If(FalseLit(), _, els) => els }, // remove trivial If conditions
+
+    )
+
+    result ++= cases.collect { case lcase if lcase.isDefinedAt(n) => lcase(n) }
+
+    result.asInstanceOf[ArrayBuffer[N]]
+  }
+
+  private def isSingleNeg[N <: Node](n: N): Boolean = n match {
+    case Not(_) => true
+    case _ => false
+  }
+
+  private def isDoubleNeg[N <: Node](n: N): Boolean = n match {
+    case Not(Not(_)) => true
+    case _ => false
+  }
+
+  protected def pfRecSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
+    val result: ArrayBuffer[N] = ArrayBuffer()
+    result ++= pfSimplify(n, assumeWelldefinedness)
+    val newChildrenList = n.children.zipWithIndex.map {
+      case (child: AtomicType, index) => {
+        ArrayBuffer()
+      }
+      case (child: N, index) => {
+        val temp = new ArrayBuffer[List[Any]]()
+        temp ++= pfRecSimplify(child, assumeWelldefinedness).toList.map { recSimpChild =>
+          n.children.toList.updated(index, recSimpChild)
+        }
+        temp
+      }
+      case _ => {
+        ArrayBuffer()
+      }
+    }
+
+    val newlist = newChildrenList.map {
+      newChildren => newChildren.map{
+        oneChildren => {
+          n.withChildren(oneChildren) }//withChildren has big performance impact!
+      }
+    }
+    newlist.map (listelem => result ++= listelem)
+    result
+  }
+
+
+  private val bigIntZero = BigInt(0)
+  private val bigIntOne = BigInt(1)
+
+  object AnyPermLiteral {
+    def unapply(p: Exp): Option[(BigInt, BigInt)] = p match {
+      case FullPerm() => Some((bigIntOne, bigIntOne))
+      case NoPerm() => Some((bigIntZero, bigIntOne))
+      case FractionalPerm(IntLit(n), IntLit(d)) => Some((n, d))
+      case _ => None
+    }
+  }
+}
+
+
+object IterativeSimplifier extends IterativeSimplifier
+
diff --git a/src/test/scala/IterativeSimplifierTest.scala b/src/test/scala/IterativeSimplifierTest.scala
new file mode 100644
index 000000000..e3ed75964
--- /dev/null
+++ b/src/test/scala/IterativeSimplifierTest.scala
@@ -0,0 +1,698 @@
+import org.scalatest.funsuite.AnyFunSuite
+import org.scalatest.matchers.should.Matchers
+import viper.silver.ast._
+import viper.silver.ast.utility.IterativeSimplifier._
+
+import scala.language.implicitConversions
+
+class IterativeSimplifierTest extends AnyFunSuite with Matchers{
+
+  test("Cmp1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(EqCmp(a,b)())()
+
+    simplify(c) should be (NeCmp(a,b)())
+  }
+
+  test("Cmp2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(NeCmp(a,b)())()
+
+    simplify(c) should be (EqCmp(a,b)())
+  }
+
+  test("Cmp3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(GtCmp(a,b)())()
+
+    simplify(c) should be (LeCmp(a,b)())
+  }
+
+  test("Cmp4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(GeCmp(a,b)())()
+
+    simplify(c) should be (LtCmp(a,b)())
+  }
+
+  test("Cmp5") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(LtCmp(a,b)())()
+
+    simplify(c) should be (GeCmp(a,b)())
+  }
+
+  test("Cmp6") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(LeCmp(a,b)())()
+
+    simplify(c) should be (GtCmp(a,b)())
+  }
+
+
+  test("notnot1") {
+    val a = LocalVar("a", Bool)()
+
+    simplify(Not(Not(a)())()) should be (a)
+  }
+
+
+  test("or1"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(FalseLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("or2"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(a, FalseLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("or3"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(TrueLit()(), a)()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+  test("or4"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(a, TrueLit()())()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+
+  test("and1") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(TrueLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("and2") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(a, TrueLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("and3") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(FalseLit()(), a)()
+
+    simplify(expr) should be (FalseLit()())
+  }
+
+  test("and4") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(a, FalseLit()())()
+
+    simplify(expr) should be (FalseLit()())
+  }
+
+  test("idem1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(And(a,b)(),a)()
+
+    simplify(expr, true) should (be (And(a,b)()) or be (And(b,a)()))
+  }
+
+  test("idem2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(b,And(a,b)())()
+
+    simplify(expr, true) should (be (And(a,b)()) or be (And(b,a)()))
+  }
+
+  test("idem3"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Or(Or(a,b)(),a)()
+
+    simplify(expr, true) should (be (Or(a,b)()) or be (Or(b,a)()))
+  }
+
+  test("idem4"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Or(b,Or(a,b)())()
+
+    simplify(expr, true) should (be (Or(a,b)()) or be (Or(b,a)()))
+  }
+
+  //while these do cannot verify if associativity of or/and is being applied, they should catch some cases where associativity is incorrectly applied
+  test("assoc1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = And(a,And(b,c)())()
+
+    simplify(expr) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
+  }
+
+  test("assoc2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = And(And(a, b)(), c)()
+
+    simplify(expr) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
+  }
+
+  test("assoc3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = Or(a,Or(b,c)())()
+
+    simplify(expr) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
+  }
+
+  test("assoc4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = Or(Or(a, b)(), c)()
+
+    simplify(expr) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
+  }
+
+  test("and11") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = And(a, And(b,c)())()
+    val expr = And(And(a,b)(), And(a,c)())()
+
+    simplify(expr, true) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
+  }
+
+  test("or11") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = Or(a, Or(b,c)())()
+    val expr = Or(Or(a,b)(), Or(a,c)())()
+
+    simplify(expr, true) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
+  }
+
+  test("impl1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(a, b)()
+
+    simplify(expr) should be (Implies(a, b)())
+  }
+
+  test("impl2") {
+    val a = FalseLit()()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(a, b)()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+  test("impl3") {
+    val a = TrueLit()()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(a, b)()
+
+    simplify(expr, true) should be (b)
+  }
+
+  test("impl4") {
+    val a = LocalVar("a", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = Implies(a,c)()
+    val expr = Implies(a, d)()
+
+    simplify(expr, true) should be (Implies(a, c)())
+  }
+
+  test("impl5") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Implies(a,b)()
+    val d = Implies(Not(a)(),b)()
+    val expr = And(c, d)()
+
+    simplify(expr, true) should be (b)
+  }
+
+  test("impl6") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Implies(a,b)()
+    val d = Implies(Not(a)(),b)()
+    val expr = And(c, d)()
+
+    simplify(expr, true) should be (b)
+  }
+
+  test("impl7") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(Not(b)(), Not(a)())()
+
+    simplify(expr) should be (Implies(a, b)())
+  }
+
+  test("and21") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Not(And(a,Not(b)())())()
+
+    simplify(expr) should be (Or(Not(a)(), b)())
+  }
+
+  test("and22") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(Not(a)(),Not(b)())()
+
+    simplify(expr) should be (Not(Or(a,b)())())
+  }
+
+  test("dem1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Not(Or(Not(a)(),Not(b)())())()
+
+    simplify(expr) should be (And(a,b)())
+  }
+
+  test("dem2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(Not(a)(),Not(b)())()
+
+    simplify(expr) should be (Not(Or(a,b)())())
+  }
+
+  test("dem3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Not(And(Not(a)(),Not(b)())())()
+
+    simplify(expr) should be (Or(a,b)())
+  }
+
+  test("dem4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Or(Not(a)(),Not(b)())()
+
+    simplify(expr) should be (Not(And(a,b)())())
+  }
+
+
+  test("eq1 assumeWelldefinedness") {
+    val x = LocalVar("x", Bool)()
+    val expr = EqCmp(x, x)()
+
+    simplify(expr, true) should be (TrueLit()())
+  }
+
+  test("eq2") {
+    val expr = EqCmp(BoolLit(true)(), BoolLit(true)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq2bis") {
+    val expr = EqCmp(BoolLit(true)(), BoolLit(false)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+
+  test("eq3") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(FalseLit()(), a)()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq4") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(a, FalseLit()())()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq5") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(TrueLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq6") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(a, TrueLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq7") {
+    val expr = EqCmp(IntLit(32)(), IntLit(32)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq7bis") {
+    val expr = EqCmp(IntLit(32)(), IntLit(31)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+
+  test("eq8") {
+    val expr = EqCmp(NullLit()(), NullLit()())()
+
+    simplify(expr) should be (TrueLit()(expr.pos, expr.info))
+  }
+
+
+
+  test("eq10") {
+    val expr = NeCmp(BoolLit(true)(), BoolLit(true)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+
+  test("eq10bis") {
+    val expr = NeCmp(BoolLit(true)(), BoolLit(false)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq11") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(FalseLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq12") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(a, FalseLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq13") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(TrueLit()(), a)()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq14") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(a, TrueLit()())()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq15") {
+    val expr = NeCmp(IntLit(32)(), IntLit(32)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+  test("eq15bis") {
+    val expr = NeCmp(IntLit(32)(), IntLit(31)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq16") {
+    val expr = NeCmp(NullLit()(), NullLit()())()
+
+    simplify(expr) should be (FalseLit()())
+  }
+
+  test("eq17 assumeWelldefinedness") {
+    val x = LocalVar("x", Bool)()
+    val expr = NeCmp(x, x)()
+
+    simplify(expr, true) should be (FalseLit()())
+  }
+  test("eq17bis assumeWelldefinedness") {
+    val expr = NeCmp(IntLit(5)(), IntLit(5)())()
+
+    simplify(expr) should be (FalseLit()())
+  }
+  test("eq17ter assumeWelldefinedness") {
+    val expr = NeCmp(IntLit(5)(), IntLit(6)())()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+
+  test("eq20 assumeWelldefinedness") {
+    val a = LocalVar("a", Int)()
+    val b = LocalVar("b", Int)()
+
+    val expr = And(
+      EqCmp(a, b)(),
+      NeCmp(a, b)()
+    )()
+
+    simplify(expr, true) should be (FalseLit()())
+  }
+
+
+  test("eq21 assumeWelldefinedness") {
+    val a = LocalVar("a", Int)()
+    val b = LocalVar("b", Int)()
+
+    val expr = Or(
+      EqCmp(a, b)(),
+      NeCmp(a, b)()
+    )()
+
+    simplify(expr, true) should be (TrueLit()())
+  }
+
+  test("ce1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val ifFalse = BoolLit(false)()
+    val expr = CondExp(TrueLit()(), a, b)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("ce2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val ifFalse = BoolLit(false)()
+    val expr = CondExp(FalseLit()(), a, b)()
+
+    simplify(expr) should be (b)
+  }
+
+  test("ce3 assumeWelldefinedness") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(b, a, a)()
+
+    simplify(expr, true) should be (a)
+  }
+
+  test("ce4") {
+    val a = LocalVar("a", Bool)()
+    val expr = CondExp(a, FalseLit()(), TrueLit()())()
+
+    simplify(expr) should be (Not(a)(expr.pos, expr.info))
+  }
+
+  test("ce5") {
+    val a = LocalVar("a", Bool)()
+    val expr = CondExp(a, TrueLit()(), FalseLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("ce6 ispure") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, FalseLit()(), Not(a)())()
+
+    println(simplify(expr))
+
+    simplify(expr) should be (Not(a)())
+  }
+  test("ce6bis assumeWelldefinedeness") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, FalseLit()(), Not(a)())()
+
+    simplify(expr, true) should be (Not(a)())
+  }
+
+  test("ce7") {
+    val a = LocalVar("a", Bool)()
+    val z = BoolLit(false)() //z must be pure/z.isPure == true
+    val expr = CondExp(a, TrueLit()(), z)()
+
+    simplify(expr) should be (a) //(a || false) = a
+  }
+
+  test("ce8") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, b, FalseLit()())()
+
+    simplify(expr) should be (And(a, b)())
+  }
+
+  test("ce9") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, b, TrueLit()())()
+
+    simplify(expr) should be (Implies(a, b)())
+  }
+
+
+
+
+
+
+
+
+
+
+
+  test("and5 assumeWelldefinedness"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = And(a, And(b,c)())()
+    val e = And(And(a,b)(), And(a,c)())()
+
+    simplify(e, true) should (be (And(And(a,b)(),c)()) or be (And(And(a,b)(),c)()))
+  }
+
+  test("implies1"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
+
+    simplify(d, true) should be (b)
+  }
+  test("not3"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
+
+    simplify(d, true) should be (b)
+  }
+  test("implies2"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = Implies(a, b)()
+
+    simplify(d) should be (d)
+  }
+  test("implies3"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val z = NullLit()()
+    val y = NullLit()()
+    val c = LocalVar("c", Bool)()
+    val aa = EqCmp(a, z)()
+    val bb = EqCmp(b, y)()
+    val d = And(Implies(aa, c)(), Implies(Not(aa)(), c)())()
+
+    simplify(d, true) should be(c)
+  }
+
+  test("test1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Or(Or(Not(a)(), Not(b)())(), FalseLit()())()
+    simplify(c) should (be (Not(And(a,b)())()) or be (Not(And(b,a)())()))
+  }
+
+  test("test14") {
+    val a = LocalVar("a", Bool)()
+    val z = LocalVar("z", Bool)()
+    val d = Or(Not(Not(a)())(), Not(Not(Not(Not(z)())())())())()
+    val f = Or(d, Not(Not(Not(Not(FalseLit()())())())())())()
+
+    simplify(f) should (be (Or(a,z)()) or be (Or(z,a)()))
+  }
+
+  test("eqcmp1") {
+    val a = LocalVar("a", Bool)()
+    val d = EqCmp(a, a)()
+    simplify(d, true) should be(TrueLit()(d.pos, d.info))
+  }
+
+  test("eqcmp2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = NeCmp(a, b)()
+    val d = EqCmp(a, b)()
+    val e = And(c, d)()
+    val f = Or(c, d)()
+
+    simplify(e, true) should be(FalseLit()(e.pos, e.info))
+    simplify(f, true) should be(TrueLit()(f.pos, f.info))
+  }
+
+  test("eqcmp3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = NeCmp(a, b)()
+    val d = EqCmp(a, b)()
+    val e = And(c, d)()
+    val f = Or(c, d)()
+
+    simplify(e, true) should be(FalseLit()(e.pos, e.info))
+    simplify(f, true) should be(TrueLit()(f.pos, f.info))
+  }
+
+  test("neue") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+
+    simplify (And(Implies(a, b)(), Implies(a, c)())()) should be (Implies(a, And(b, c)())())
+
+    simplify (And(Implies(a, b)(), Implies(Not(a)(), b)())()) should be (And(Implies(a,b)(),Implies(Not(a)(), b)())())
+    simplify (And(Implies(a, b)(), Implies(Not(a)(), b)())(), true) should be (b)
+
+    simplify (And(a, Implies(a, b)())()) should be (And(a, b)())
+  }
+
+  test("neue2") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+
+    println(simplify(And(a, And(And(a,b)(), c)())(), true, 5000, true))
+
+    true should be (true)
+  }
+
+
+
+
+}