diff --git a/silver b/silver
index d6161459c..231b73fb5 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit d6161459c32f58c47c162a467ea675fdfac8fd17
+Subproject commit 231b73fb515b38547bc434ed0b9c94d969edc129
diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index 9f3061735..41c31f442 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -568,6 +568,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
             proverArgs.flatMap(args => proverTimeoutArg findFirstMatchIn args map(_.group(1).toInt))}
         .getOrElse(0)
 
+  lazy val useFlyweight: Boolean = prover() == "Z3-API"
+
   val maxHeuristicsDepth: ScallopOption[Int] = opt[Int]("maxHeuristicsDepth",
     descr = "Maximal number of nested heuristics applications (default: 3)",
     default = Some(3),
diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
index 9c27fc4e9..29e284443 100644
--- a/src/main/scala/decider/Decider.scala
+++ b/src/main/scala/decider/Decider.scala
@@ -120,7 +120,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     private def getProver(prover: String): Prover = prover match {
       case Z3ProverStdIO.name => new Z3ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
       case Cvc5ProverStdIO.name => new Cvc5ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
-      case Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter)
+      case Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter, triggerGenerator)
       case prover =>
         val msg1 = s"Unknown prover '$prover' provided. Defaulting to ${Z3ProverStdIO.name}."
         logger warn msg1
@@ -273,10 +273,10 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     }
 
     private def isKnownToBeTrue(t: Term) = t match {
-      case True() => true
+      case True => true
   //    case eq: BuiltinEquals => eq.p0 == eq.p1 /* WARNING: Blocking trivial equalities might hinder axiom triggering. */
       case _ if pcs.assumptions contains t => true
-      case q: Quantification if q.body == True() => true
+      case q: Quantification if q.body == True => true
       case _ => false
     }
 
@@ -382,7 +382,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def statistics(): Map[String, String] = prover.statistics()
 
-    override def generateModel(): Unit = proverAssert(False(), None)
+    override def generateModel(): Unit = proverAssert(False, None)
 
     override def getModel(): Model = prover.getModel()
 
diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
index 7eb3fd1f5..8f53ac589 100644
--- a/src/main/scala/decider/PathConditions.scala
+++ b/src/main/scala/decider/PathConditions.scala
@@ -143,7 +143,7 @@ private trait LayeredPathConditionStackLike {
   protected def conditionalized(layers: Stack[PathConditionStackLayer]): Seq[Term] = {
     var unconditionalTerms = Vector.empty[Term]
     var conditionalTerms = Vector.empty[Term]
-    var implicationLHS: Term = True()
+    var implicationLHS: Term = True
 
     for (layer <- layers.reverseIterator) {
       unconditionalTerms ++= layer.globalAssumptions
@@ -182,7 +182,7 @@ private trait LayeredPathConditionStackLike {
         Quantification(
           quantifier,
           qvars,
-          Implies(layer.branchCondition.getOrElse(True()), And(layer.nonGlobalAssumptions -- ignores)),
+          Implies(layer.branchCondition.getOrElse(True), And(layer.nonGlobalAssumptions -- ignores)),
           triggers,
           name,
           isGlobal)
diff --git a/src/main/scala/decider/TermToSMTLib2Converter.scala b/src/main/scala/decider/TermToSMTLib2Converter.scala
index 7868dbfa4..7540d15e3 100644
--- a/src/main/scala/decider/TermToSMTLib2Converter.scala
+++ b/src/main/scala/decider/TermToSMTLib2Converter.scala
@@ -197,8 +197,8 @@ class TermToSMTLib2Converter
 
     /* Permissions */
 
-    case FullPerm() => "$Perm.Write"
-    case NoPerm() => "$Perm.No"
+    case FullPerm => "$Perm.Write"
+    case NoPerm => "$Perm.No"
     case FractionPermLiteral(r) => renderBinaryOp("/", renderAsReal(IntLiteral(r.numerator)), renderAsReal(IntLiteral(r.denominator)))
     case FractionPerm(n, d) => renderBinaryOp("/", renderAsReal(n), renderAsReal(d))
     case PermLess(t0, t1) => renderBinaryOp("<", render(t0), render(t1))
@@ -370,9 +370,9 @@ class TermToSMTLib2Converter
       else parens(text("- 0") <+> value(-n))
 
     case Unit => "$Snap.unit"
-    case True() => "true"
-    case False() => "false"
-    case Null() => "$Ref.null"
+    case True => "true"
+    case False => "false"
+    case Null => "$Ref.null"
     case _: SeqNil => renderApp("Seq_empty", Seq(), literal.sort)
     case _: EmptySet => renderApp("Set_empty", Seq(), literal.sort)
     case _: EmptyMultiset => renderApp("Multiset_empty", Seq(), literal.sort)
diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala
index 0560a5dd6..8cf6d83fe 100644
--- a/src/main/scala/decider/TermToZ3APIConverter.scala
+++ b/src/main/scala/decider/TermToZ3APIConverter.scala
@@ -30,6 +30,7 @@ class TermToZ3APIConverter
 
   val sortCache = mutable.HashMap[Sort, Z3Sort]()
   val funcDeclCache = mutable.HashMap[(String, Seq[Sort], Sort), Z3FuncDecl]()
+  val termCache = mutable.HashMap[Term, Z3Expr]()
 
   def convert(s: Sort): Z3Sort = convertSort(s)
 
@@ -203,6 +204,9 @@ class TermToZ3APIConverter
 
 
   def convertTerm(term: Term): Z3Expr = {
+    val cached = termCache.get(term)
+    if (cached.isDefined)
+      return cached.get
     val res = term match {
       case l: Literal => {
         l match {
@@ -212,9 +216,9 @@ class TermToZ3APIConverter
             else
               ctx.mkUnaryMinus(ctx.mkInt((-n).toString()))
           }
-          case True() => ctx.mkTrue()
-          case False() => ctx.mkFalse()
-          case Null() => ctx.mkConst("$Ref.null", ctx.mkUninterpretedSort("$Ref"))
+          case True => ctx.mkTrue()
+          case False => ctx.mkFalse()
+          case Null => ctx.mkConst("$Ref.null", ctx.mkUninterpretedSort("$Ref"))
           case Unit => ctx.mkConst(getUnitConstructor)
           case _: SeqNil => createApp("Seq_empty", Seq(), l.sort)
           case _: EmptySet => createApp("Set_empty", Seq(), l.sort)
@@ -254,11 +258,13 @@ class TermToZ3APIConverter
         } else{
           val qvarExprs = vars.map(v => convert(v)).toArray
           val nonEmptyTriggers = triggers.filter(_.p.nonEmpty)
-          val patterns = if (nonEmptyTriggers.nonEmpty)
-              // Simplify trigger terms; Z3 does this automatically when used via stdio, and it sometimes makes
-              // triggers valid that would otherwise be rejected.
-              nonEmptyTriggers.map(t => ctx.mkPattern(t.p.map(trm => convertTerm(trm).simplify()): _*)).toArray
-            else null
+          val patterns = if (nonEmptyTriggers.nonEmpty) {
+              // ME: Maybe we should simplify trigger terms here? There is some evidence that Z3 does this
+              // automatically when used via stdio, and it sometimes makes triggers valid that would otherwise be
+              // rejected. On the other hand, it's not at all obvious that simplification does not change the shape
+              // of a trigger term, which would not be what we want.
+              nonEmptyTriggers.map(t => ctx.mkPattern(t.p.map(trm => convertTerm(trm)): _*)).toArray
+          } else null
           val weightValue = weight.getOrElse(1)
           if (quant == Forall) {
             ctx.mkForall(qvarExprs, convertTerm(body), weightValue, patterns, null, ctx.mkSymbol(name), null)
@@ -310,8 +316,8 @@ class TermToZ3APIConverter
       /* Permissions */
 
 
-      case FullPerm() => ctx.mkReal(1)
-      case NoPerm() => ctx.mkReal(0)
+      case FullPerm => ctx.mkReal(1)
+      case NoPerm => ctx.mkReal(0)
       case FractionPermLiteral(r) => ctx.mkDiv(convertToReal(IntLiteral(r.numerator)), convertToReal(IntLiteral(r.denominator)))
       case FractionPerm(n, d) => ctx.mkDiv(convertToReal(n), convertToReal(d))
       case PermLess(t0, t1) => ctx.mkLt(convertTerm(t0).asInstanceOf[ArithExpr], convertTerm(t1).asInstanceOf[ArithExpr])
@@ -441,6 +447,7 @@ class TermToZ3APIConverter
          | _: Quantification =>
         sys.error(s"Unexpected term $term cannot be translated to SMTLib code")
     }
+    termCache.put(term, res)
     res
   }
 
@@ -516,6 +523,7 @@ class TermToZ3APIConverter
     macros.clear()
     funcDeclCache.clear()
     sortCache.clear()
+    termCache.clear()
     unitConstructor = null
     combineConstructor = null
     firstFunc = null
diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala
index 4ba20dce2..ed98ee7ba 100644
--- a/src/main/scala/decider/Z3ProverAPI.scala
+++ b/src/main/scala/decider/Z3ProverAPI.scala
@@ -9,17 +9,19 @@ package viper.silicon.decider
 import com.typesafe.scalalogging.LazyLogging
 import viper.silicon.common.config.Version
 import viper.silicon.interfaces.decider.{Prover, Result, Sat, Unknown, Unsat}
-import viper.silicon.state.IdentifierFactory
-import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Sort, SortDecl, SortWrapperDecl, Term, sorts}
+import viper.silicon.state.{IdentifierFactory, State}
+import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, Trigger, TriggerGenerator, sorts}
 import viper.silicon.{Config, Map}
 import viper.silicon.verifier.Verifier
 import viper.silver.reporter.{InternalWarningMessage, Reporter}
 import viper.silver.verifier.{MapEntry, ModelEntry, ModelParser, ValueEntry, DefaultDependency => SilDefaultDependency, Model => ViperModel}
+
 import java.io.PrintWriter
 import java.nio.file.Path
-
 import scala.collection.mutable
 import com.microsoft.z3._
+import com.microsoft.z3.enumerations.Z3_param_kind
+import viper.silicon.decider.Z3ProverAPI.oldVersionOnlyParams
 import viper.silicon.reporting.ExternalToolError
 
 import scala.jdk.CollectionConverters.MapHasAsJava
@@ -28,8 +30,8 @@ import scala.util.Random
 
 object Z3ProverAPI {
   val name = "Z3-API"
-  val minVersion = Version("4.8.6.0")
-  val maxVersion = Some(Version("4.8.7.0")) /* X.Y.Z if that is the *last supported* version */
+  val minVersion = Version("4.8.7.0")
+  val maxVersion = Some(Version("4.12.1.0")) /* X.Y.Z if that is the *last supported* version */
 
   // these are not actually used, but since there is a lot of code that expects command line parameters and a
   // config file, we just supply this information here (whose contents will then be ignored)
@@ -46,34 +48,31 @@ object Z3ProverAPI {
   val initialOptions = Map("auto_config" -> "false", "type_check" -> "true")
   val boolParams = Map(
     "smt.delay_units" -> true,
-    "delay_units" -> true,
     "smt.mbqi" -> false,
-    "mbqi" -> false,
     //"pp.bv_literals" -> false,  // This is part of z3config.smt2 but Z3 won't accept it via API.
     "model.v2" -> true
   )
   val intParams = Map(
     "smt.case_split" -> 3,
-    "case_split" -> 3,
     "smt.qi.max_multi_patterns" -> 1000,
-    "qi.max_multi_patterns" -> 1000,
     "smt.arith.solver" -> 2,
-    "arith.solver" -> 2
   )
   val stringParams: Map[String, String] = Map(
     // currently none
   )
   val doubleParams = Map(
     "smt.qi.eager_threshold" -> 100.0,
-    "qi.eager_threshold" -> 100.0,
   )
+  val allParams = boolParams ++ intParams ++ stringParams ++ doubleParams
+  val oldVersionOnlyParams = Set("smt.arith.solver")
 }
 
 
 class Z3ProverAPI(uniqueId: String,
                   termConverter: TermToZ3APIConverter,
                   identifierFactory: IdentifierFactory,
-                  reporter: Reporter)
+                  reporter: Reporter,
+                  triggerGenerator: TriggerGenerator)
     extends Prover
       with LazyLogging
 {
@@ -114,19 +113,59 @@ class Z3ProverAPI(uniqueId: String,
     lastTimeout = -1
     ctx = new Context(Z3ProverAPI.initialOptions.asJava)
     val params = ctx.mkParams()
+
+    // When setting parameters via API, we have to remove the smt. prefix
+    def removeSmtPrefix(s: String) = {
+      if (s.startsWith("smt."))
+        s.substring(4)
+      else
+        s
+    }
+
+    val useOldVersionParams = version() <= Version("4.8.7.0")
     Z3ProverAPI.boolParams.foreach{
-      case (k, v) => params.add(k, v)
+      case (k, v) =>
+        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
+          params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.intParams.foreach{
-      case (k, v) => params.add(k, v)
+      case (k, v) =>
+        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
+          params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.doubleParams.foreach{
-      case (k, v) => params.add(k, v)
+      case (k, v) =>
+        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
+          params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.stringParams.foreach{
-      case (k, v) => params.add(k, v)
+      case (k, v) =>
+        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
+          params.add(removeSmtPrefix(k), v)
     }
+    val userProvidedArgs = Verifier.config.proverConfigArgs
     prover = ctx.mkSolver()
+    val descrs = prover.getParameterDescriptions
+    for ((origKey, vl) <- userProvidedArgs) {
+      val key = if (origKey.startsWith("smt."))
+        origKey.substring(4)
+      else
+        origKey
+      val keySymbol = ctx.mkSymbol(key)
+      val param_kind = descrs.getKind(keySymbol)
+      param_kind match {
+        case Z3_param_kind.Z3_PK_BOOL =>
+          params.add(key, vl.toBoolean)
+        case Z3_param_kind.Z3_PK_UINT =>
+          params.add(key, vl.toInt)
+        case Z3_param_kind.Z3_PK_DOUBLE =>
+          params.add(key, vl.toDouble)
+        case Z3_param_kind.Z3_PK_STRING =>
+          params.add(key, vl)
+        case _ =>
+          reporter.report(InternalWarningMessage("Z3 error: unknown parameter" + key))
+      }
+    }
     prover.setParameters(params)
     termConverter.start()
     termConverter.ctx = ctx
@@ -212,7 +251,21 @@ class Z3ProverAPI(uniqueId: String,
       else
         preambleAssumes.add(termConverter.convert(term).asInstanceOf[BoolExpr])
     } catch {
-      case e: Z3Exception => reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage))
+      case e: Z3Exception =>
+        // The only reason we get an exception here is that we've tried to assume a quantifier with an invalid trigger.
+        // When used via API, Z3 completely discards assumptions that contain invalid triggers (whereas it just ignores
+        // the invalid trigger when used via stdio). Thus, to make sure our assumption is not discarded, we manually
+        // walk through all quantifiers and remove invalid terms inside the trigger.
+        triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger)
+        val cleanTerm = term.transform{
+          case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty =>
+            val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect{
+              case t => triggerGenerator.isForbiddenInTrigger(t)
+            }.nonEmpty))
+            q.copy(triggers = goodTriggers)
+        }()
+        prover.add(termConverter.convert(cleanTerm).asInstanceOf[BoolExpr])
+        reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage))
     }
   }
 
@@ -316,7 +369,13 @@ class Z3ProverAPI(uniqueId: String,
     if (!preamblePhaseOver) {
       preamblePhaseOver = true
 
-      val merged = emittedPreambleString.mkString("\n")
+      // Setting all options again , since otherwise some of them seem to get lost.
+      val standardOptionPrefix = Seq("(set-option :auto_config false)", "(set-option :type_check true)") ++
+        Z3ProverAPI.allParams.map(bp => s"(set-option :${bp._1} ${bp._2})")
+
+      val customOptionPrefix = Verifier.config.proverConfigArgs.map(a => s"(set-option :${a._1} ${a._2})")
+
+      val merged = (standardOptionPrefix ++ customOptionPrefix ++ emittedPreambleString).mkString("\n")
       val parsed = ctx.parseSMTLIB2String(merged, emittedSortSymbols.toArray, emittedSorts.toArray, emittedFuncSymbols.toArray, emittedFuncs.toArray)
       prover.add(parsed: _*)
       prover.add(preambleAssumes.toSeq : _*)
diff --git a/src/main/scala/reporting/Converter.scala b/src/main/scala/reporting/Converter.scala
index c41f6edef..b4e2fedbd 100644
--- a/src/main/scala/reporting/Converter.scala
+++ b/src/main/scala/reporting/Converter.scala
@@ -151,7 +151,7 @@ object Converter {
   lazy val symbolConverter: SymbolConverter = new DefaultSymbolConverter
   //some tokens used for naming model entries in a more maintainable way
   lazy val snapUnitId: String = termconverter.convert(Unit)
-  lazy val nullRefId: String = termconverter.convert(Null())
+  lazy val nullRefId: String = termconverter.convert(Null)
 
   def getFunctionValue(model: Model,
                        fname: String,
@@ -254,7 +254,7 @@ object Converter {
       case Unit              => UnprocessedModelEntry(ConstantEntry(snapUnitId))
       case IntLiteral(x)     => LitIntEntry(x)
       case t: BooleanLiteral => LitBoolEntry(t.value)
-      case Null()            => VarEntry(model.entries(nullRefId).toString, sorts.Ref)
+      case Null              => VarEntry(model.entries(nullRefId).toString, sorts.Ref)
       case Var(_, sort) =>
         val key: String = term.toString
         val entry: Option[ModelEntry] = model.entries.get(key)
@@ -416,8 +416,8 @@ object Converter {
         case _ => None
       }
       case App(_, _) => None
-      case NoPerm() => Some(Rational.zero)
-      case FullPerm() => Some(Rational.one)
+      case NoPerm => Some(Rational.zero)
+      case FullPerm => Some(Rational.one)
       case FractionPermLiteral(r) => Some(r)
       case _: FractionPerm => None
       case IsValidPermVar(_) => None
diff --git a/src/main/scala/reporting/Formatters.scala b/src/main/scala/reporting/Formatters.scala
index a8cd164e1..f7248fe49 100644
--- a/src/main/scala/reporting/Formatters.scala
+++ b/src/main/scala/reporting/Formatters.scala
@@ -58,7 +58,7 @@ class DefaultStateFormatter extends StateFormatter {
       case    c: BuiltinEquals if c.p0.isInstanceOf[Combine]
            || c.p1.isInstanceOf[Combine]
            => true
-      case Not(BuiltinEquals(_, Null())) => true
+      case Not(BuiltinEquals(_, Null)) => true
       case _ => false
     }.mkString("(", ", ", ")")
   }
@@ -92,7 +92,7 @@ class DefaultStateFormatter extends StateFormatter {
     val filteredPcs = pcs.filterNot {
       case c: BuiltinEquals if c.p0.isInstanceOf[Combine]
         || c.p1.isInstanceOf[Combine] => true
-      case Not(BuiltinEquals(_, Null())) => true
+      case Not(BuiltinEquals(_, Null)) => true
       case _ => false
     }
     if (filteredPcs.isEmpty) "[]" else filteredPcs.mkString("[\"", "\",\"", "\"]")
diff --git a/src/main/scala/resources/PropertyInterpreter.scala b/src/main/scala/resources/PropertyInterpreter.scala
index 7d86dbc3b..ebaa2d9c0 100644
--- a/src/main/scala/resources/PropertyInterpreter.scala
+++ b/src/main/scala/resources/PropertyInterpreter.scala
@@ -14,10 +14,10 @@ abstract class PropertyInterpreter {
 
   protected def buildPathCondition[K <: Kind](expression: PropertyExpression[K], info: Info): Term = expression match {
     // Literals
-    case True() => terms.True()
-    case False() => terms.False()
+    case True() => terms.True
+    case False() => terms.False
     case PermissionLiteral(numerator, denominator) => buildPermissionLiteral(numerator, denominator)
-    case Null() => terms.Null()
+    case Null() => terms.Null
 
     // Boolean operators
     case Not(expr) => terms.Not(buildPathCondition(expr, info))
@@ -62,7 +62,7 @@ abstract class PropertyInterpreter {
    the right-hand side is not evaluated. */
   protected def buildAnd(left: PropertyExpression[kinds.Boolean], right: PropertyExpression[kinds.Boolean], info: Info) = {
     buildPathCondition(left, info) match {
-      case leftTerm: terms.False => leftTerm
+      case f@terms.False => f
       case leftTerm => terms.And(leftTerm, buildPathCondition(right, info))
     }
   }
@@ -71,7 +71,7 @@ abstract class PropertyInterpreter {
    the right-hand side is not evaluated. */
   protected def buildOr(left: PropertyExpression[kinds.Boolean], right: PropertyExpression[kinds.Boolean], info: Info) = {
     buildPathCondition(left, info) match {
-      case leftTerm: terms.True => leftTerm
+      case t@terms.True => t
       case leftTerm => terms.Or(leftTerm, buildPathCondition(right, info))
     }
   }
@@ -80,26 +80,26 @@ abstract class PropertyInterpreter {
    the right-hand side is not evaluated. */
   protected def buildImplies(left: PropertyExpression[kinds.Boolean], right: PropertyExpression[kinds.Boolean], info: Info) = {
     buildPathCondition(left, info) match {
-      case terms.False() => terms.True()
+      case terms.False => terms.True
       case leftTerm => terms.Implies(leftTerm, buildPathCondition(right, info))
     }
   }
 
   protected def buildEquals[K <: EquatableKind](left: PropertyExpression[K], right: PropertyExpression[K], info: Info) = {
     (left, right) match {
-      case (Null(), Null()) => terms.True()
+      case (Null(), Null()) => terms.True
       case (ArgumentAccess(cv1), ArgumentAccess(cv2)) =>
         val args1 = extractArguments(cv1, info)
         val args2 = extractArguments(cv2, info)
         if (args1 == args2) {
           // if all arguments are the same, they are definitely equal
-          terms.True()
+          terms.True
         } else {
           // else return argument-wise equal
           terms.And(args1.zip(args2).map{ case (t1, t2) => t1 === t2 })
         }
-      case (ArgumentAccess(cv), Null()) => terms.And(extractArguments(cv, info).map(_ === terms.Null()))
-      case (Null(), ArgumentAccess(cv)) => terms.And(extractArguments(cv, info).map(_ === terms.Null()))
+      case (ArgumentAccess(cv), Null()) => terms.And(extractArguments(cv, info).map(_ === terms.Null))
+      case (Null(), ArgumentAccess(cv)) => terms.And(extractArguments(cv, info).map(_ === terms.Null))
       case _ => terms.Equals(buildPathCondition(left, info), buildPathCondition(right, info))
     }
   }
@@ -109,17 +109,26 @@ abstract class PropertyInterpreter {
   protected def buildPermissionLiteral(numerator: BigInt, denominator: BigInt): Term = {
     require(denominator != 0, "Denominator of permission literal must not be 0")
     (numerator, denominator) match {
-      case (n, _) if n == 0 => terms.NoPerm()
-      case (n, d) if n == d => terms.FullPerm()
+      case (n, _) if n == 0 => terms.NoPerm
+      case (n, d) if n == d => terms.FullPerm
       case (n, d) => terms.FractionPerm(terms.IntLiteral(n), terms.IntLiteral(d))
     }
   }
 
+  protected def buildBinary[K <: Kind]
+                           (builder: ((Term, Term)) => Term,
+                            left: PropertyExpression[K],
+                            right: PropertyExpression[K],
+                            pm: Info): Term = {
+    def wrapper(t0: Term, t1: Term): Term = builder((t0, t1))
+    buildBinary(wrapper _, left, right, pm)
+  }
+
   protected def buildBinary[K <: Kind]
                            (builder: (Term, Term) => Term,
                             left: PropertyExpression[K],
                             right: PropertyExpression[K],
-                            pm: Info) = {
+                            pm: Info): Term = {
     val leftTerm = buildPathCondition(left, pm)
     val rightTerm = buildPathCondition(right, pm)
     builder(leftTerm, rightTerm)
diff --git a/src/main/scala/resources/QuantifiedPropertyInterpreter.scala b/src/main/scala/resources/QuantifiedPropertyInterpreter.scala
index 2f0ebfcce..3a72ee4dd 100644
--- a/src/main/scala/resources/QuantifiedPropertyInterpreter.scala
+++ b/src/main/scala/resources/QuantifiedPropertyInterpreter.scala
@@ -27,7 +27,7 @@ class QuantifiedPropertyInterpreter extends PropertyInterpreter {
                                 : Term = {
     val body = buildPathCondition(property.expression, Info(chunk, args, perms)).replace(chunk.quantifiedVars, args)
     val description = s"$qidPrefix-${property.name}"
-    val cond = if (argsUsed) condition else terms.True()
+    val cond = if (argsUsed) condition else terms.True
     argsUsed = false
     terms.Forall(qvars, terms.Implies(cond, body), triggers, description)
   }
diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala
index c394da325..fe88e765b 100644
--- a/src/main/scala/rules/ChunkSupporter.scala
+++ b/src/main/scala/rules/ChunkSupporter.scala
@@ -159,13 +159,13 @@ object chunkSupporter extends ChunkSupportRules {
           val newChunk = ch.withPerm(PermMinus(ch.perm, toTake))
           val takenChunk = Some(ch.withPerm(toTake))
           var newHeap = h - ch
-          if (!v.decider.check(newChunk.perm === NoPerm(), Verifier.config.checkTimeout())) {
+          if (!v.decider.check(newChunk.perm === NoPerm, Verifier.config.checkTimeout())) {
             newHeap = newHeap + newChunk
             assumeProperties(newChunk, newHeap)
           }
           (ConsumptionResult(PermMinus(perms, toTake), v, 0), s, newHeap, takenChunk)
         } else {
-          if (v.decider.check(ch.perm !== NoPerm(), Verifier.config.checkTimeout())) {
+          if (v.decider.check(ch.perm !== NoPerm, Verifier.config.checkTimeout())) {
             v.decider.assume(PermLess(perms, ch.perm))
             val newChunk = ch.withPerm(PermMinus(ch.perm, perms))
             val takenChunk = ch.withPerm(perms)
@@ -177,7 +177,7 @@ object chunkSupporter extends ChunkSupportRules {
           }
         }
       case None =>
-        if (consumeExact && s.retrying && v.decider.check(perms === NoPerm(), Verifier.config.checkTimeout())) {
+        if (consumeExact && s.retrying && v.decider.check(perms === NoPerm, Verifier.config.checkTimeout())) {
           (Complete(), s, h, None)
         } else {
           (Incomplete(perms), s, h, None)
diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
index d337f572c..ac1a95edc 100644
--- a/src/main/scala/rules/Consumer.scala
+++ b/src/main/scala/rules/Consumer.scala
@@ -290,7 +290,7 @@ object consumer extends ConsumptionRules {
           if (forall.triggers.isEmpty) None
           else Some(forall.triggers)
         val ePerm = ast.FullPerm()()
-        val tPerm = FullPerm()
+        val tPerm = FullPerm
         evalQuantified(s, Forall, forall.variables, Seq(cond), bodyVars, optTrigger, qid, pve, v) {
           case (s1, qvars, Seq(tCond), tArgs, tTriggers, (auxGlobals, auxNonGlobals), v1) =>
             quantifiedChunkSupporter.consume(
@@ -421,7 +421,7 @@ object consumer extends ConsumptionRules {
           } else {
             s1
           }
-          val loss = PermTimes(FullPerm(), s1.permissionScalingFactor)
+          val loss = PermTimes(FullPerm, s1.permissionScalingFactor)
           quantifiedChunkSupporter.consumeSingleLocation(
             s1p,
             h,
@@ -441,7 +441,7 @@ object consumer extends ConsumptionRules {
         magicWandSupporter.evaluateWandArguments(s, wand, pve, v)((s1, tArgs, v1) => {
           val ve = pve dueTo MagicWandChunkNotFound(wand)
           val description = s"consume wand $wand"
-          chunkSupporter.consume(s1, h, wand, tArgs, FullPerm(), ve, v1, description)(Q)
+          chunkSupporter.consume(s1, h, wand, tArgs, FullPerm, ve, v1, description)(Q)
         })
 
       case _ =>
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 64aae33e2..fc456abbc 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -150,10 +150,10 @@ object evaluator extends EvaluationRules {
                      : VerificationResult = {
 
     val resultTerm = e match {
-      case _: ast.TrueLit => Q(s, True(), v)
-      case _: ast.FalseLit => Q(s, False(), v)
+      case _: ast.TrueLit => Q(s, True, v)
+      case _: ast.FalseLit => Q(s, False, v)
 
-      case _: ast.NullLit => Q(s, Null(), v)
+      case _: ast.NullLit => Q(s, Null, v)
       case ast.IntLit(bigval) => Q(s, IntLiteral(bigval), v)
 
       case ast.EqCmp(e0, e1) => evalBinOp(s, e0, e1, Equals, pve, v)(Q)
@@ -161,8 +161,8 @@ object evaluator extends EvaluationRules {
 
       case x: ast.AbstractLocalVar => Q(s, s.g(x), v)
 
-      case _: ast.FullPerm => Q(s, FullPerm(), v)
-      case _: ast.NoPerm => Q(s, NoPerm(), v)
+      case _: ast.FullPerm => Q(s, FullPerm, v)
+      case _: ast.NoPerm => Q(s, NoPerm, v)
 
       case ast.FractionalPerm(e0, e1) =>
         var t1: Term = null
@@ -242,7 +242,7 @@ object evaluator extends EvaluationRules {
               }
               val permCheck =
                 if (s1.triggerExp) {
-                  True()
+                  True
                 } else {
                   val totalPermissions = PermLookup(fa.field.name, pmDef1.pm, tRcvr)
                   IsPositive(totalPermissions)
@@ -386,7 +386,7 @@ object evaluator extends EvaluationRules {
 
       case ast.PermMinus(e0) =>
         eval(s, e0, pve, v)((s1, t0, v1) =>
-          Q(s1, PermMinus(NoPerm(), t0), v1))
+          Q(s1, PermMinus(NoPerm, t0), v1))
 
       case ast.PermMul(e0, e1) =>
         evalBinOp(s, e0, e1, PermTimes, pve, v)(Q)
@@ -482,7 +482,7 @@ object evaluator extends EvaluationRules {
                   }
                   val currentPermAmount = PermLookup(field.name, pmDef.pm, args.head)
                   v1.decider.prover.comment(s"perm($resacc)  ~~>  assume upper permission bound")
-                  v1.decider.assume(PermAtMost(currentPermAmount, FullPerm()))
+                  v1.decider.assume(PermAtMost(currentPermAmount, FullPerm))
                   (s2, currentPermAmount)
 
                 case predicate: ast.Predicate =>
@@ -500,9 +500,9 @@ object evaluator extends EvaluationRules {
             } else {
               val chs = chunkSupporter.findChunksWithID[NonQuantifiedChunk](h.values, identifier)
               val currentPermAmount =
-                chs.foldLeft(NoPerm(): Term)((q, ch) => {
+                chs.foldLeft(NoPerm: Term)((q, ch) => {
                   val argsPairWiseEqual = And(args.zip(ch.args).map { case (a1, a2) => a1 === a2 })
-                  PermPlus(q, Ite(argsPairWiseEqual, ch.perm, NoPerm()))
+                  PermPlus(q, Ite(argsPairWiseEqual, ch.perm, NoPerm))
                 })
               /* TODO: See todo above */
 //              v1.decider.prover.comment(s"perm($locacc)  ~~>  assume upper permission bound")
@@ -556,7 +556,7 @@ object evaluator extends EvaluationRules {
               val zippedArgs = argsWithIndex map (ai => (ai._1, ch.args(ai._2)))
               val argsPairWiseEqual = And(zippedArgs map {case (a1, a2) => a1 === a2})
 
-              evalImplies(s3, Ite(argsPairWiseEqual, And(addCons :+ IsPositive(ch.perm)), False()), None,body, false, pve, v1) ((s4, tImplies, v2) =>
+              evalImplies(s3, Ite(argsPairWiseEqual, And(addCons :+ IsPositive(ch.perm)), False), None,body, false, pve, v1) ((s4, tImplies, v2) =>
                 bindRcvrsAndEvalBody(s4, chs.tail, args, tImplies +: ts, v2)((s5, ts1, v3) => {
                   v3.symbExLog.closeScope(uidImplies)
                   Q(s5, ts1, v3)
@@ -1073,11 +1073,11 @@ object evaluator extends EvaluationRules {
     joiner.join[Term, Term](s, v)((s1, v1, QB) =>
       brancher.branch(s1, tLhs, eLhs, v1, fromShortCircuitingAnd)(
         (s2, v2) => eval(s2, eRhs, pve, v2)(QB),
-        (s2, v2) => QB(s2, True(), v2))
+        (s2, v2) => QB(s2, True, v2))
     )(entries => {
       assert(entries.length <= 2)
       val s1 = entries.tail.foldLeft(entries.head.s)((sAcc, entry) => sAcc.merge(entry.s))
-      val t = Implies(tLhs, entries.headOption.map(_.data).getOrElse(True()))
+      val t = Implies(tLhs, entries.headOption.map(_.data).getOrElse(True))
       (s1, t)
     })(Q)
   }
@@ -1134,6 +1134,18 @@ object evaluator extends EvaluationRules {
     }
   }
 
+  private def evalBinOp[T <: Term](s: State,
+                                   e0: ast.Exp,
+                                   e1: ast.Exp,
+                                   termOp: ((Term, Term)) => T,
+                                   pve: PartialVerificationError,
+                                   v: Verifier)
+                                  (Q: (State, T, Verifier) => VerificationResult)
+                                  : VerificationResult = {
+
+    evalBinOp(s, e0, e1, (t0, t1) => termOp((t0, t1)), pve, v)(Q)
+  }
+
   private def evalBinOp[T <: Term]
                        (s: State,
                         e0: ast.Exp,
@@ -1532,8 +1544,8 @@ object evaluator extends EvaluationRules {
 
     // TODO: Find out and document why swapIfAnd is needed
     val (stop, swapIfAnd) =
-      if(constructor == Or) (True(), (a: brFun, b: brFun) => (a, b))
-      else (False(), (a: brFun, b: brFun) => (b, a))
+      if(constructor == Or) (True, (a: brFun, b: brFun) => (a, b))
+      else (False, (a: brFun, b: brFun) => (b, a))
 
     eval(s, exps.head, pve, v)((s1, t0, v1) => {
       t0 match {
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 407611f44..24d2c602d 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -330,7 +330,7 @@ object executor extends ExecutionRules {
               Seq(`?r`),
               `?r` === tRcvr,
               field,
-              FullPerm(),
+              FullPerm,
               chunkOrderHeuristics,
               v2
             )
@@ -340,7 +340,7 @@ object executor extends ExecutionRules {
                 val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s3, field, Seq(tRcvr), tRhs, v2)
                 v1.decider.prover.comment("Definitional axioms for singleton-FVF's value")
                 v1.decider.assume(smValueDef)
-                val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm(), sm, s.program)
+                val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm, sm, s.program)
                 if (s3.heapDependentTriggers.contains(field))
                   v1.decider.assume(FieldTrigger(field.name, sm, tRcvr))
                 Q(s3.copy(h = h3 + ch), v2)
@@ -355,10 +355,10 @@ object executor extends ExecutionRules {
             val resource = fa.res(s.program)
             val ve = pve dueTo InsufficientPermission(fa)
             val description = s"consume ${ass.pos}: $ass"
-            chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), FullPerm(), ve, v2, description)((s3, h3, _, v3) => {
+            chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), FullPerm, ve, v2, description)((s3, h3, _, v3) => {
               val tSnap = ssaifyRhs(tRhs, field.name, field.typ, v3)
               val id = BasicChunkIdentifier(field.name)
-              val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), tSnap, FullPerm())
+              val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), tSnap, FullPerm)
               chunkSupporter.produce(s3, h3, newChunk, v3)((s4, h4, v4) =>
                 Q(s4.copy(h = h4), v4))
             })
@@ -367,9 +367,9 @@ object executor extends ExecutionRules {
 
       case ast.NewStmt(x, fields) =>
         val tRcvr = v.decider.fresh(x)
-        v.decider.assume(tRcvr !== Null())
+        v.decider.assume(tRcvr !== Null)
         val newChunks = fields map (field => {
-          val p = FullPerm()
+          val p = FullPerm
           val snap = v.decider.fresh(field.name, v.symbolConverter.toSort(field.typ))
           if (s.qpFields.contains(field)) {
             val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, field, Seq(tRcvr), snap, v)
diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala
index 63520ae22..ec2ea7cfe 100644
--- a/src/main/scala/rules/HavocSupporter.scala
+++ b/src/main/scala/rules/HavocSupporter.scala
@@ -116,7 +116,7 @@ object havocSupporter extends SymbolicExecutionRules {
           quantifiedChunkSupporter.injectivityAxiom(
             qvars     = tVars,
             condition = tCond,
-            perms     = FullPerm(),
+            perms     = FullPerm,
             arguments = tArgs,
             triggers  = Nil,
             qidPrefix = qid,
diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala
index 5e0bbf3d3..8b509f3a6 100644
--- a/src/main/scala/rules/MagicWandSupporter.scala
+++ b/src/main/scala/rules/MagicWandSupporter.scala
@@ -106,7 +106,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
                  (Q: (State, MagicWandChunk, Verifier) => VerificationResult)
                  : VerificationResult = {
     evaluateWandArguments(s, wand, pve, v)((s1, ts, v1) =>
-      Q(s1, MagicWandChunk(MagicWandIdentifier(wand, s.program), s1.g.values, ts, snap, FullPerm()), v1)
+      Q(s1, MagicWandChunk(MagicWandIdentifier(wand, s.program), s1.g.values, ts, snap, FullPerm), v1)
     )
   }
 
@@ -155,10 +155,10 @@ object magicWandSupporter extends SymbolicExecutionRules {
                * and thus be unsound. Since fractional wands do not exist it is not necessary to equate their
                * snapshots. Also have a look at the comments in the packageWand and applyWand methods.
                */
-              case (Some(_: MagicWandChunk), Some(_: MagicWandChunk)) => True()
+              case (Some(_: MagicWandChunk), Some(_: MagicWandChunk)) => True
               case (Some(ch1: NonQuantifiedChunk), Some(ch2: NonQuantifiedChunk)) => ch1.snap === ch2.snap
               case (Some(ch1: QuantifiedBasicChunk), Some(ch2: QuantifiedBasicChunk)) => ch1.snapshotMap === ch2.snapshotMap
-              case _ => True()
+              case _ => True
             }
             v.decider.assume(tEq)
 
@@ -297,7 +297,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
             quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, MagicWandSnapshot(freshSnapRoot, snap), v4)
           v4.decider.prover.comment("Definitional axioms for singleton-SM's value")
           v4.decider.assume(smValueDef)
-          val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm(), sm, s.program)
+          val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm, sm, s.program)
           appendToResults(s5, ch, v4.decider.pcs.after(preMark), v4)
           Success()
         })
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
index 9cdf7528a..1a9f18b51 100644
--- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
+++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -59,7 +59,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
     val `?s` = Var(Identifier("?s"), sort)
     var summarisingSnapshotDefinitions: Seq[Term] = Vector.empty
-    var permissionSum: Term = NoPerm()
+    var permissionSum: Term = NoPerm
 
     relevantChunks.foreach(ch => {
       val argumentEqualities =
@@ -69,7 +69,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         Implies(And(argumentEqualities, IsPositive(ch.perm)), `?s` === ch.snap)
 
       permissionSum =
-        PermPlus(permissionSum, Ite(argumentEqualities, ch.perm, NoPerm()))
+        PermPlus(permissionSum, Ite(argumentEqualities, ch.perm, NoPerm))
     })
 
     val taggedSummarisingSnapshot =
@@ -109,7 +109,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
       if (v.decider.check(And(chunk.args.zip(args).map { case (t1, t2) => t1 === t2 }), Verifier.config.checkTimeout())) {
         return Q(s, chunk.snap, Seq(), chunk.perm, v)
       } else {
-        return Q(s, chunk.snap, Seq(), NoPerm(), v)
+        return Q(s, chunk.snap, Seq(), NoPerm, v)
       }
     }
     val (s1, taggedSnap, snapDefs, permSum) = summariseOnly(s, relevantChunks, resource, args, v)
@@ -217,7 +217,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
     if (relevantChunks.isEmpty) {
       // if no permission is exhaled, return none
-      v.decider.assert(perms === NoPerm()){
+      v.decider.assert(perms === NoPerm) {
         case true => Q(s, h, None, v)
         case false => createFailure(ve, v, s)
       }
@@ -227,7 +227,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
           Q(s1, Heap(updatedChunks ++ otherChunks), optSnap, v2)})
       } else {
         var pNeeded = perms
-        var pSum: Term = NoPerm()
+        var pSum: Term = NoPerm
         val newChunks = ListBuffer[NonQuantifiedChunk]()
         var moreNeeded = true
 
@@ -245,15 +245,24 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         relevantChunks.sortWith(sortFunction) foreach { ch =>
           if (moreNeeded) {
             val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 })
-            pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm()))
-            val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm())
-            val pTakenArgs = additionalArgs
-            val pTakenDecl = v.decider.freshMacro("mce_pTaken", pTakenArgs, pTakenBody)
-            val pTakenMacro = Macro(pTakenDecl.id, pTakenDecl.args.map(_.sort), pTakenDecl.body.sort)
-            val pTaken = App(pTakenMacro, pTakenArgs)
 
-            currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(pTakenDecl)
-            v.symbExLog.addMacro(pTaken, pTakenBody)
+            val pTaken = if (Verifier.config.useFlyweight) {
+              // ME: When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different
+              // (leading to new terms that have to be translated), whereas without macros, we can usually use a term
+              // that already exists.
+              Ite(eq, PermMin(ch.perm, pNeeded), NoPerm)
+            } else {
+              val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm)
+              val pTakenArgs = additionalArgs
+              val pTakenDecl = v.decider.freshMacro("mce_pTaken", pTakenArgs, pTakenBody)
+              val pTakenMacro = Macro(pTakenDecl.id, pTakenDecl.args.map(_.sort), pTakenDecl.body.sort)
+              currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(pTakenDecl)
+              val pTakenApp = App(pTakenMacro, pTakenArgs)
+              v.symbExLog.addMacro(pTakenApp, pTakenBody)
+              pTakenApp
+            }
+
+            pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm))
 
             val newChunk = ch.withPerm(PermMinus(ch.perm, pTaken))
             pNeeded = PermMinus(pNeeded, pTaken)
@@ -262,7 +271,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
               newChunks.append(newChunk)
             }
 
-            moreNeeded = !v.decider.check(pNeeded === NoPerm(), Verifier.config.splitTimeout())
+            moreNeeded = !v.decider.check(pNeeded === NoPerm, Verifier.config.splitTimeout())
           } else {
             newChunks.append(ch)
           }
@@ -289,7 +298,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
           if (!moreNeeded) {
             Q(s1, newHeap, Some(condSnap), v1)
           } else {
-            v1.decider.assert(pNeeded === NoPerm()) {
+            v1.decider.assert(pNeeded === NoPerm) {
               case true =>
                 Q(s1, newHeap, Some(condSnap), v1)
               case false =>
@@ -310,8 +319,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
                                                 (Q: (State, ListBuffer[NonQuantifiedChunk], Option[Term], Verifier) => VerificationResult)
                                                 : VerificationResult = {
 
-    var totalPermSum: Term = NoPerm()
-    var totalPermTaken: Term = NoPerm()
+    var totalPermSum: Term = NoPerm
+    var totalPermTaken: Term = NoPerm
     var newFr = s.functionRecorder
 
     val updatedChunks =
@@ -319,12 +328,12 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 })
         val permTaken = v.decider.fresh("p", sorts.Perm)
 
-        totalPermSum = PermPlus(totalPermSum, Ite(eq, ch.perm, NoPerm()))
+        totalPermSum = PermPlus(totalPermSum, Ite(eq, ch.perm, NoPerm))
         totalPermTaken = PermPlus(totalPermTaken, permTaken)
 
         val constraint = And(IsValidPermVar(permTaken),
           PermAtMost(permTaken, ch.perm),
-          Implies(Not(eq), permTaken === NoPerm())
+          Implies(Not(eq), permTaken === NoPerm)
         )
 
         v.decider.assume(constraint)
@@ -335,14 +344,14 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
     v.decider.assume(
       Implies(
-        totalPermSum !== NoPerm(),
+        totalPermSum !== NoPerm,
         And(
-          PermLess(NoPerm(), totalPermTaken),
+          PermLess(NoPerm, totalPermTaken),
           PermLess(totalPermTaken, totalPermSum))))
 
     val s1 = s.copy(functionRecorder = newFr)
 
-    v.decider.assert(totalPermTaken !== NoPerm()) {
+    v.decider.assert(totalPermTaken !== NoPerm) {
       case true =>
         v.decider.assume(perms === totalPermTaken)
         summarise(s1, relevantChunks.toSeq, resource, args, v)((s2, snap, _, _, v1) =>
@@ -371,14 +380,14 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
     relevantChunksPerField foreach { case (_, relevantChunks) =>
       val permissionSum =
-        relevantChunks.foldLeft(NoPerm(): Term) { case (permSum, chunk) =>
+        relevantChunks.foldLeft(NoPerm: Term) { case (permSum, chunk) =>
           val eq = freeReceiver === chunk.args.head /* For field chunks, the receiver is the only argument */
-          PermPlus(permSum, Ite(eq, chunk.perm, NoPerm()))
+          PermPlus(permSum, Ite(eq, chunk.perm, NoPerm))
         }
 
       relevantChunks foreach (chunk => {
         val instantiatedPermSum = permissionSum.replace(freeReceiver, chunk.args.head)
-        v.decider.assume(PermAtMost(instantiatedPermSum, FullPerm()))
+        v.decider.assume(PermAtMost(instantiatedPermSum, FullPerm))
       })
     }
   }
diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala
index 2c6e1f251..a29672f59 100644
--- a/src/main/scala/rules/Producer.scala
+++ b/src/main/scala/rules/Producer.scala
@@ -160,7 +160,7 @@ object producer extends ProductionRules {
           // We will get an IllegalArgumentException from createSnapshotPair if sf(...) returns Unit.
           // This should never happen if we're in a reachable state, so here we check for that
           // (without timeout, since there is no fallback) and stop verifying the current branch.
-          case _: IllegalArgumentException if v.decider.check(False(), Verifier.config.assertTimeout.getOrElse(0)) =>
+          case _: IllegalArgumentException if v.decider.check(False, Verifier.config.assertTimeout.getOrElse(0)) =>
             Unreachable()
         }
 
@@ -306,7 +306,7 @@ object producer extends ProductionRules {
             if (s1.recordPcs) (s1.conservedPcs.head :+ v1.decider.pcs.after(definitionalAxiomMark)) +: s1.conservedPcs.tail
             else s1.conservedPcs
           val ch =
-            quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm(), sm, s.program)
+            quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm, sm, s.program)
           val h2 = s1.h + ch
           val smCache1 = if(s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s1.program))){
             val (relevantChunks, _) =
@@ -421,7 +421,7 @@ object producer extends ProductionRules {
               tCond,
               tArgs,
               tSnap,
-              FullPerm(),
+              FullPerm,
               pve,
               NegativePermission(ast.FullPerm()()),
               QPAssertionNotInjective(wand),
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index 5d94239dd..6d3c5fc4a 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -225,7 +225,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           .map { case (x, a) => x === a })
 
     val conditionalizedPermissions =
-      Ite(condition, permissions, NoPerm())
+      Ite(condition, permissions, NoPerm)
 
     val hints = extractHints(None, arguments)
 
@@ -274,7 +274,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       Ite(
         And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)),
         permissions.replace(qvarsToInversesOfCodomain),
-        NoPerm())
+        NoPerm)
 
     val hints = extractHints(Some(condition), arguments)
 
@@ -424,7 +424,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val additionalFvfArgs = s.functionRecorderQuantifiedVariables()
     val sm = freshSnapshotMap(s, field, additionalFvfArgs, v)
 
-    val smDomainDefinitionCondition = optSmDomainDefinitionCondition.getOrElse(True())
+    val smDomainDefinitionCondition = optSmDomainDefinitionCondition.getOrElse(True)
     val codomainQVarsInDomainOfSummarisingSm = SetIn(codomainQVar, Domain(field.name, sm))
 
     val valueDefinitions =
@@ -520,7 +520,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
         val effectiveCondition =
           And(
-            transformedOptSmDomainDefinitionCondition.getOrElse(True()), /* Alternatively: qvarInDomainOfSummarisingSm */
+            transformedOptSmDomainDefinitionCondition.getOrElse(True), /* Alternatively: qvarInDomainOfSummarisingSm */
             IsPositive(chunk.perm).replace(snapToCodomainTermsSubstitution))
 
         Forall(
@@ -877,7 +877,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               qidPrefix = qid,
               program   = s.program)
           } else {
-            True()
+            True
           }
         v.decider.prover.comment("Check receiver injectivity")
         v.decider.assume(FunctionPreconditionTransformer.transform(receiverInjectivityCheck, s.program))
@@ -1261,7 +1261,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             codomainQVars,
             relevantChunks,
             v1,
-            optSmDomainDefinitionCondition = if (s2.smDomainNeeded) Some(True()) else None,
+            optSmDomainDefinitionCondition = if (s2.smDomainNeeded) Some(True) else None,
             optQVarsInstantiations = Some(arguments))
         val permsTaken = result match {
           case Complete() => rPerm
@@ -1305,7 +1305,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               resource = resource,
               codomainQVars = codomainQVars,
               relevantChunks = relevantChunks,
-              optSmDomainDefinitionCondition = if (s1.smDomainNeeded) Some(True()) else None,
+              optSmDomainDefinitionCondition = if (s1.smDomainNeeded) Some(True) else None,
               optQVarsInstantiations = Some(arguments),
               v = v)
           val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1),
@@ -1359,7 +1359,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
     val precomputedData = candidates map { ch =>
       val permsProvided = ch.perm
-      val permsTakenBody = Ite(condition, PermMin(permsProvided, permsNeeded), NoPerm())
+      val permsTakenBody = Ite(condition, PermMin(permsProvided, permsNeeded), NoPerm)
       val permsTakenArgs = codomainQVars ++ additionalArgs
       val permsTakenDecl = v.decider.freshMacro("pTaken", permsTakenArgs, permsTakenBody)
       val permsTakenMacro = Macro(permsTakenDecl.id, permsTakenDecl.args.map(_.sort), permsTakenDecl.body.sort)
@@ -1376,7 +1376,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     v.decider.prover.comment(s"Done precomputing, updating quantified chunks")
     v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.beforeIteration)
 
-    var tookEnoughCheck = Forall(codomainQVars, Implies(condition, permsNeeded === NoPerm()), Nil)
+    var tookEnoughCheck = Forall(codomainQVars, Implies(condition, permsNeeded === NoPerm), Nil)
 
     precomputedData foreach { case (ithChunk, ithPTaken, ithPNeeded) =>
       if (success.isComplete)
@@ -1408,7 +1408,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
          * the assertion to check is recorded by tookEnoughCheck.
          */
         tookEnoughCheck =
-          Forall(codomainQVars, Implies(condition, ithPNeeded === NoPerm()), Nil)
+          Forall(codomainQVars, Implies(condition, ithPNeeded === NoPerm), Nil)
 
         v.decider.prover.comment(s"Intermediate check if already taken enough permissions")
         success = if (v.decider.check(tookEnoughCheck, Verifier.config.splitTimeout())) {
@@ -1442,7 +1442,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                                                         : (Term, Term) = {
 
     val conditionalizedPerms =
-      Ite(condition, perms, NoPerm()) // c(rs) ? p(rs) : none
+      Ite(condition, perms, NoPerm) // c(rs) ? p(rs) : none
 
     val quantifiedPermissionConstraint =
       if (!constrainPermissions) {
@@ -1453,7 +1453,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           Forall(
             codomainQVars,
             Implies(
-              ithChunk.perm !== NoPerm(),
+              ithChunk.perm !== NoPerm,
               PermLess(conditionalizedPerms, ithChunk.perm)),
             Nil,
             s"qp.srp${v.counter(this).next()}")
@@ -1466,7 +1466,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       }
 
     val quantifiedDepletedCheck =
-      Forall(codomainQVars, PermMinus(ithChunk.perm, ithPTaken) === NoPerm(), Nil)
+      Forall(codomainQVars, PermMinus(ithChunk.perm, ithPTaken) === NoPerm, Nil)
 
     val (permissionConstraint, depletedCheck) =
       ithChunk.singletonArguments match {
@@ -1478,7 +1478,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
              quantifiedDepletedCheck)
         }
 
-    (permissionConstraint.getOrElse(True()), depletedCheck)
+    (permissionConstraint.getOrElse(True), depletedCheck)
   }
 
   /* Misc */
@@ -1554,7 +1554,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
     val argsEqual: Term =
       if (args1.isEmpty)
-        True()
+        True
       else
         (args1 zip args2)
             .map(argsRenamed =>  argsRenamed._1 === argsRenamed._2)
@@ -1631,8 +1631,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         imagesOfCodomains(idx) = img(codomainQVars)
       } else {
         // imageFunctions(idx) remains null, will be filtered out later.
-        imagesOfFcts(idx) = True()
-        imagesOfCodomains(idx) = True()
+        imagesOfFcts(idx) = True
+        imagesOfCodomains(idx) = True
       }
     }
 
diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala
index 373076b8a..ba207cefe 100644
--- a/src/main/scala/rules/StateConsolidator.scala
+++ b/src/main/scala/rules/StateConsolidator.scala
@@ -207,8 +207,8 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
     */
   private def combineSnapshots(fr: FunctionRecorder, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
     (IsPositive(p1), IsPositive(p2)) match {
-      case (True(), b2) => (fr, t1, Implies(b2, t1 === t2))
-      case (b1, True()) => (fr, t2, Implies(b1, t2 === t1))
+      case (True, b2) => (fr, t1, Implies(b2, t1 === t2))
+      case (b1, True) => (fr, t2, Implies(b1, t2 === t1))
       case (b1, b2) =>
         /*
          * Since it is not definitely known whether p1 and p2 are positive,
@@ -245,7 +245,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
           val currentPermAmount = PermLookup(field.name, pmDef.pm, receiver)
           v.decider.prover.comment(s"Assume upper permission bound for field ${field.name}")
           v.decider.assume(
-            Forall(receiver, PermAtMost(currentPermAmount, FullPerm()), Trigger(trigger), "qp-fld-prm-bnd"))
+            Forall(receiver, PermAtMost(currentPermAmount, FullPerm), Trigger(trigger), "qp-fld-prm-bnd"))
         } else {
           /*
           If we don't use heap-dependent triggers, the trigger x.f does not work. Instead, we assume the permission
@@ -255,14 +255,14 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
            */
           for (chunk <- fieldChunks) {
             if (chunk.singletonRcvr.isDefined){
-              v.decider.assume(PermAtMost(PermLookup(field.name, pmDef.pm, chunk.singletonRcvr.get), FullPerm()))
+              v.decider.assume(PermAtMost(PermLookup(field.name, pmDef.pm, chunk.singletonRcvr.get), FullPerm))
             } else {
               val chunkReceivers = chunk.invs.get.inverses.map(i => App(i, chunk.invs.get.additionalArguments ++ chunk.quantifiedVars))
               val triggers = chunkReceivers.map(r => Trigger(r)).toSeq
               val currentPermAmount = PermLookup(field.name, pmDef.pm, chunk.quantifiedVars.head)
               v.decider.prover.comment(s"Assume upper permission bound for field ${field.name}")
               v.decider.assume(
-                Forall(chunk.quantifiedVars, PermAtMost(currentPermAmount, FullPerm()), triggers, "qp-fld-prm-bnd"))
+                Forall(chunk.quantifiedVars, PermAtMost(currentPermAmount, FullPerm), triggers, "qp-fld-prm-bnd"))
             }
 
           }
diff --git a/src/main/scala/state/FunctionPreconditionTransformer.scala b/src/main/scala/state/FunctionPreconditionTransformer.scala
index c21d23dfa..515d917b3 100644
--- a/src/main/scala/state/FunctionPreconditionTransformer.scala
+++ b/src/main/scala/state/FunctionPreconditionTransformer.scala
@@ -23,7 +23,7 @@ import viper.silver.ast
 object FunctionPreconditionTransformer {
   def transform(t: Term, p: ast.Program): Term = {
     val res = t match {
-      case _:Literal => True()
+      case _:Literal => True
       case And(ts) => And(transform(ts.head, p), Implies(ts.head, transform(And(ts.tail), p)))
       case Or(ts) => And(transform(ts.head, p), Implies(Not(ts.head), transform(Or(ts.tail), p)))
       case Implies(t0, t1) => And(transform(t0, p), Implies(t0, transform(t1, p)))
@@ -32,7 +32,7 @@ object FunctionPreconditionTransformer {
         And(And(bindings.map(b => transform(b._2, p))), Let(bindings, transform(body, p)))
       case Quantification(_, vars, body, triggers, name, isGlobal, weight) =>
         val tBody = transform(body, p)
-        if (tBody == True()) {
+        if (tBody == True) {
           tBody
         } else {
           // We assume well-definedness for *all* possible values even for existential quantifiers
diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 4703d34ea..56a3f29e3 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -45,7 +45,7 @@ final case class State(g: Store = Store(),
                        triggerExp: Boolean = false,
 
                        partiallyConsumedHeap: Option[Heap] = None,
-                       permissionScalingFactor: Term = terms.FullPerm(),
+                       permissionScalingFactor: Term = terms.FullPerm,
 
                        reserveHeaps: Stack[Heap] = Nil,
                        reserveCfgs: Stack[SilverCfg] = Stack(),
diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala
index ccc59b4e5..bcda3f8f3 100644
--- a/src/main/scala/state/Terms.scala
+++ b/src/main/scala/state/Terms.scala
@@ -7,13 +7,14 @@
 package viper.silicon.state.terms
 
 import java.util.concurrent.atomic.AtomicInteger
-
 import scala.annotation.tailrec
 import scala.reflect.ClassTag
 import viper.silver.ast
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.{Map, Stack, state, toMap}
 import viper.silicon.state.{Identifier, MagicWandChunk, MagicWandIdentifier, SortBasedIdentifier}
+import viper.silicon.verifier.Verifier
+import scala.collection.concurrent.TrieMap
 
 sealed trait Node {
   def toString: String
@@ -94,19 +95,40 @@ sealed trait Decl extends Node {
   def id: Identifier
 }
 
-case class SortDecl(sort: Sort) extends Decl {
+class SortDecl private[terms] (val sort: Sort) extends Decl with ConditionalFlyweight[Sort, SortDecl] {
   val id: Identifier = sort.id
+  override val equalityDefiningMembers: Sort = sort
+}
+
+object SortDecl extends CondFlyweightFactory[Sort, SortDecl, SortDecl] {
+  override def actualCreate(args: Sort): SortDecl = new SortDecl(args)
 }
 
-case class FunctionDecl(func: Function) extends Decl {
+class FunctionDecl private[terms] (val func: Function) extends Decl with ConditionalFlyweight[Function, FunctionDecl] {
   val id: Identifier = func.id
+  override val equalityDefiningMembers: Function = func
+}
+
+object FunctionDecl extends CondFlyweightFactory[Function, FunctionDecl, FunctionDecl] {
+  override def actualCreate(args: Function): FunctionDecl = new FunctionDecl(args)
 }
 
-case class SortWrapperDecl(from: Sort, to: Sort) extends Decl {
+class SortWrapperDecl private[terms] (val from: Sort, val to: Sort) extends Decl with ConditionalFlyweight[(Sort, Sort), SortWrapperDecl] {
   val id: Identifier = SortWrapperId(from, to)
+  override val equalityDefiningMembers: (Sort, Sort) = (from, to)
 }
 
-case class MacroDecl(id: Identifier, args: Seq[Var], body: Term) extends Decl
+object SortWrapperDecl extends CondFlyweightFactory[(Sort, Sort), SortWrapperDecl, SortWrapperDecl] {
+  override def actualCreate(args: (Sort, Sort)): SortWrapperDecl = new SortWrapperDecl(args._1, args._2)
+}
+
+class MacroDecl private[terms] (val id: Identifier, val args: Seq[Var], val body: Term) extends Decl with ConditionalFlyweight[(Identifier, Seq[Var], Term), MacroDecl] {
+  override val equalityDefiningMembers: (Identifier, Seq[Var], Term) = (id, args, body)
+}
+
+object MacroDecl extends CondFlyweightFactory[(Identifier, Seq[Var], Term), MacroDecl, MacroDecl] {
+  override def actualCreate(args: (Identifier, Seq[Var], Term)): MacroDecl = new MacroDecl(args._1, args._2, args._3)
+}
 
 object ConstDecl extends (Var => Decl) { /* TODO: Inconsistent naming - Const vs Var */
   def apply(v: Var) = FunctionDecl(v)
@@ -142,8 +164,8 @@ object Function {
  *      (i.e. field) that indicates the kind of
  */
 
-trait GenericFunction[F <: Function] extends Function with StructuralEquality {
-  val equalityDefiningMembers = id +: argSorts :+ resultSort
+trait GenericFunction[F <: Function] extends Function {
+  val equalityDefiningMembers = (id, argSorts, resultSort)
 
   def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort): F
 
@@ -157,20 +179,19 @@ trait GenericFunctionCompanion[F <: Function] {
 
   def apply(id: Identifier, argSort: Sort, resultSort: Sort): F =
     apply(id, Seq(argSort), resultSort)
-
-  def unapply(fun: F): Some[(Identifier, Seq[Sort], Sort)] =
-    Some((fun.id, fun.argSorts, fun.resultSort))
 }
 
-class Fun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort)
-    extends GenericFunction[Fun] {
+class Fun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort)
+    extends ConditionalFlyweight[(Identifier, Seq[Sort], Sort), Fun] with GenericFunction[Fun] {
 
   def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) =
     Fun(id, argSorts, resultSort)
 }
 
-object Fun extends ((Identifier, Seq[Sort], Sort) => Fun) with GenericFunctionCompanion[Fun] {
-  def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = new Fun(id, argSorts, resultSort)
+object Fun extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), Fun, Fun] with GenericFunctionCompanion[Fun] {
+  def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort))
+
+  override def actualCreate(args: (Identifier, Seq[Sort], Sort)): Fun = new Fun(args._1, args._2, args._3)
 }
 
 /* TODO: [18-12-2015 Malte] Since heap-dependent functions are represented by a separate class,
@@ -178,59 +199,79 @@ object Fun extends ((Identifier, Seq[Sort], Sort) => Fun) with GenericFunctionCo
  *       toLimited/toStateless, and to remove the corresponding methods from the FunctionSupporter
  *       object.
  */
-class HeapDepFun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort)
-    extends GenericFunction[HeapDepFun] {
+class HeapDepFun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort)
+    extends ConditionalFlyweight[(Identifier, Seq[Sort], Sort), HeapDepFun] with GenericFunction[HeapDepFun] {
 
   def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) =
     HeapDepFun(id, argSorts, resultSort)
 }
 
-object HeapDepFun extends ((Identifier, Seq[Sort], Sort) => HeapDepFun) with GenericFunctionCompanion[HeapDepFun] {
-  def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = new HeapDepFun(id, argSorts, resultSort)
+object HeapDepFun extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), HeapDepFun, HeapDepFun] with GenericFunctionCompanion[HeapDepFun] {
+  def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort))
+
+  override def actualCreate(args: (Identifier, Seq[Sort], Sort)): HeapDepFun = new HeapDepFun(args._1, args._2, args._3)
 }
 
-class DomainFun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort)
-    extends GenericFunction[DomainFun] {
+class DomainFun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort)
+    extends ConditionalFlyweight[(Identifier, Seq[Sort], Sort), DomainFun] with GenericFunction[DomainFun] {
 
   def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) =
     DomainFun(id, argSorts, resultSort)
 }
 
-object DomainFun extends ((Identifier, Seq[Sort], Sort) => DomainFun) with GenericFunctionCompanion[DomainFun] {
-  def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = new DomainFun(id, argSorts, resultSort)
+object DomainFun extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), DomainFun, DomainFun] with GenericFunctionCompanion[DomainFun] {
+  def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort))
+
+  override def actualCreate(args: (Identifier, Seq[Sort], Sort)): DomainFun = new DomainFun(args._1, args._2, args._3)
 }
 
-class SMTFun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort)
-  extends GenericFunction[SMTFun] {
+class SMTFun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort)
+  extends ConditionalFlyweight[(Identifier, Seq[Sort], Sort), SMTFun] with GenericFunction[SMTFun] {
 
   def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) =
    SMTFun(id, argSorts, resultSort)
 }
 
-object SMTFun extends ((Identifier, Seq[Sort], Sort) => SMTFun) with GenericFunctionCompanion[SMTFun] {
-  def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = new SMTFun(id, argSorts, resultSort)
+object SMTFun extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), SMTFun, SMTFun] with GenericFunctionCompanion[SMTFun] {
+  def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort))
+
+  override def actualCreate(args: (Identifier, Seq[Sort], Sort)): SMTFun = new SMTFun(args._1, args._2, args._3)
+}
+
+class Macro private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) extends Applicable
+  with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), Macro] {
+  override val equalityDefiningMembers: (Identifier, Seq[Sort], Sort) = (id, argSorts, resultSort)
 }
 
-case class Macro(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) extends Applicable
+object Macro extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), Macro, Macro] {
+  override def actualCreate(args: (Identifier, Stack[Sort], Sort)): Macro = new Macro(args._1, args._2, args._3)
+}
 
-case class Var(id: Identifier, sort: Sort) extends Function with Application[Var] {
+class Var private[terms] (val id: Identifier, val sort: Sort) extends Function with Application[Var] with ConditionalFlyweight[(Identifier, Sort), Var] {
+  override val equalityDefiningMembers: (Identifier, Sort) = (id, sort)
   val applicable: Var = this
   val args: Seq[Term] = Seq.empty
   val argSorts: Seq[Sort] = Seq(sorts.Unit)
   val resultSort: Sort = sort
 
   override lazy val toString = id.toString
+
+  def copy(id: Identifier = id, sort: Sort = sort) = Var(id, sort)
+}
+
+object Var extends CondFlyweightFactory[(Identifier, Sort), Var, Var] {
+  override def actualCreate(args: (Identifier, Sort)): Var = new Var(args._1, args._2)
 }
 
-class App(val applicable: Applicable, val args: Seq[Term])
+class App private[terms] (val applicable: Applicable, val args: Seq[Term])
     extends Application[Applicable]
-       with StructuralEquality {
+       with ConditionalFlyweight[(Applicable, Seq[Term]), App] {
        /*with PossibleTrigger*/
 
   utils.assertExpectedSorts(applicable, args)
 
   val sort: Sort = applicable.resultSort
-  val equalityDefiningMembers = applicable +: args
+  val equalityDefiningMembers = (applicable, args)
   def copy(applicable: Applicable = applicable, args: Seq[Term] = args) = App(applicable, args)
 
   override lazy val toString =
@@ -238,10 +279,11 @@ class App(val applicable: Applicable, val args: Seq[Term])
     else s"${applicable.id}${args.mkString("(", ", ", ")")}"
 }
 
-object App extends ((Applicable, Seq[Term]) => App) {
-  def apply(applicable: Applicable, args: Seq[Term]) = new App(applicable, args)
-  def apply(applicable: Applicable, arg: Term) = new App(applicable, Seq(arg))
-  def unapply(app: App) = Some((app.applicable, app.args))
+object App extends CondFlyweightTermFactory[(Applicable, Seq[Term]), App] {
+  def apply(applicable: Applicable, args: Seq[Term]) = createIfNonExistent((applicable, args))
+  def apply(applicable: Applicable, arg: Term) = createIfNonExistent((applicable, Seq(arg)))
+
+  override def actualCreate(args: (Applicable, Seq[Term])): App = new App(args._1, args._2)
 }
 
 /*
@@ -383,6 +425,25 @@ trait BinaryOp[E] {
   override lazy val toString = s"$p0 $op $p1"
 }
 
+/**
+  * Trait that implements equality and hashCode based on the equality of the equalityDefiningMembers value.
+  * Used to implement case class like behavior for ordinary classes.
+  * No longer used and superseded by the ConditionalFlyweight trait, but kept here for documentation purposes.
+  */
+trait StructuralEquality { self: AnyRef =>
+  val equalityDefiningMembers: Seq[Any]
+
+  override val hashCode = viper.silver.utility.Common.generateHashCode(equalityDefiningMembers)
+
+  override def equals(other: Any) = (
+    this.eq(other.asInstanceOf[AnyRef])
+      || (other match {
+      case se: StructuralEquality if this.getClass.eq(se.getClass) =>
+        equalityDefiningMembers == se.equalityDefiningMembers
+      case _ => false
+    }))
+}
+
 trait StructuralEqualityUnaryOp[E] extends UnaryOp[E] {
   override def equals(other: Any) =
     this.eq(other.asInstanceOf[AnyRef]) || (other match {
@@ -408,20 +469,118 @@ trait StructuralEqualityBinaryOp[E] extends BinaryOp[E] {
   override def hashCode(): Int = p0.hashCode() * p1.hashCode()
 }
 
-trait StructuralEquality { self: AnyRef =>
-  val equalityDefiningMembers: Seq[Any]
+/**
+  * A trait that defines equality and hashcode in such a way that:
+  * 1. if Verifier.config.useFlyweight is set, then both are computed using references
+  * 2. otherwise, both are computed based on equality of the equalityDefiningMembers value.
+  * See also trait StructuralEquality above.
+  * The motivation for this is to use the flyweight pattern when Z3 is used via its API, in which case it is
+  * advantageous to have only a single version of each Silicon term (since this enables check caching of their
+  * Z3 translations, and repeatedly translating the same Silicon term to a Z3 expression massively reduces performance
+  * for large files), but to avoid the overhead of the flyweight pattern otherwise (since it costs time to check
+  * for existing copies of a term, and there is no benefit to this when Z3 or some other SMT solver is used via
+  * StdIO.
+  *
+  * @tparam T the type of the constructor parameters of the class (i.e., a tuple or a single parameter type)
+  * @tparam V the type of the class implementing the trait
+  */
+trait ConditionalFlyweight[T, V] { self: AnyRef =>
+  // The single value or tuple of values that define equality
+  val equalityDefiningMembers: T
+
+  override lazy val hashCode = if (Verifier.config.useFlyweight)
+    System.identityHashCode(this)
+  else
+    viper.silver.utility.Common.generateHashCode(equalityDefiningMembers)
+
+  override def equals(other: Any): Boolean = {
+    if (Verifier.config.useFlyweight) {
+      this.eq(other.asInstanceOf[AnyRef])
+    } else {
+      (
+        this.eq(other.asInstanceOf[AnyRef])
+          || (other match {
+          case se: ConditionalFlyweight[T, V] if this.getClass.eq(se.getClass) =>
+            equalityDefiningMembers == se.equalityDefiningMembers
+          case _ => false
+        }))
+    }
+  }
 
-  override val hashCode = viper.silver.utility.Common.generateHashCode(equalityDefiningMembers)
+  override lazy val toString: String = {
+    val argString = equalityDefiningMembers match {
+      case p: Product =>
+        p.productIterator.mkString(", ")
+      case trm => trm.toString
+    }
+    s"${this.getClass.getSimpleName}(${argString})"
+  }
+}
 
-  override def equals(other: Any) = (
-    this.eq(other.asInstanceOf[AnyRef])
-      || (other match {
-      case se: StructuralEquality if this.getClass.eq(se.getClass) =>
-        equalityDefiningMembers == se.equalityDefiningMembers
-      case _ => false
-    }))
+trait ConditionalFlyweightBinaryOp[T] extends ConditionalFlyweight[(Term, Term), T] with BinaryOp[Term] with Term {
+  override val equalityDefiningMembers = (p0,  p1)
+}
+
+trait ConditionalFlyweightUnaryOp[T] extends ConditionalFlyweight[Term, T] with UnaryOp[Term] with Term {
+  override val equalityDefiningMembers = p
+}
+
+/**
+  * Version of CondFlyweightFactory where the return type of apply is Term, i.e., the apply method may return
+  * arbitrary terms due to simplification.
+  * @tparam T constructor argument type of the class V (i.e., a tuple or the type of the only argument)
+  * @tparam V class we are creating instances of
+  */
+trait CondFlyweightTermFactory[T, V <: ConditionalFlyweight[T, V] with Term] extends CondFlyweightFactory[T, Term, V]
+
+/**
+  * Version of CondFlyweightFactory where the return type of apply is V, i.e., the apply method always returns an
+  * instance of the class whose apply method is called.
+  * @tparam T constructor argument type of the class V (i.e., a tuple or the type of the only argument)
+  * @tparam V class we are creating instances of
+  */
+trait PreciseCondFlyweightFactory[T, V <: ConditionalFlyweight[T, V] with Term] extends CondFlyweightFactory[T, V, V]
+
+
+/**
+  * Default version of GeneralCondFlyweightFactory where the arguments of the apply method is the same as the
+  * constructor arguments of class V.
+  * @tparam T constructor argument type of the class V (i.e., a tuple or the type of the only argument)
+  * @tparam U return type of the apply method (i.e., either the class itself or something more general for simplifying
+  *           apply methods)
+  * @tparam V class we are creating instances of
+  */
+trait CondFlyweightFactory[T, U, V <: U with ConditionalFlyweight[T, V]] extends GeneralCondFlyweightFactory[T, T, U, V] {
+  def apply(v1: T): U = createIfNonExistent(v1)
+
+}
+
+/**
+  * Most general trait to be implemented by companion objects to create instances of ConditionalFlyweight[T, V].
+  * @tparam IF parameter type of the apply method (can be different from the constructor args of the class)
+  * @tparam T constructor argument type of the class V (i.e., a tuple or the type of the only argument)
+  * @tparam U return type of the apply method (i.e., either the class itself or something more general for simplifying
+  *           apply methods)
+  * @tparam V class we are creating instances of
+  */
+trait GeneralCondFlyweightFactory[IF, T <: IF, U, V <: U with ConditionalFlyweight[T, V]] extends (IF => U) {
+
+  var pool = new TrieMap[T, V]()
+
+  def createIfNonExistent(args: T): V = {
+    if (Verifier.config.useFlyweight) {
+      pool.getOrElseUpdate(args, actualCreate(args))
+    } else {
+      actualCreate(args)
+    }
+  }
+
+  def unapply(v: V): Option[T] = Some(v.equalityDefiningMembers)
+
+  def actualCreate(args: T): V
 }
 
+
 /* Literals */
 
 sealed trait Literal extends Term
@@ -430,15 +589,19 @@ case object Unit extends SnapshotTerm with Literal {
   override lazy val toString = "_"
 }
 
-case class IntLiteral(n: BigInt) extends ArithmeticTerm with Literal {
+class IntLiteral private[terms] (val n: BigInt) extends ArithmeticTerm with Literal with ConditionalFlyweight[BigInt, IntLiteral] {
   def +(m: Int) = IntLiteral(n + m)
   def -(m: Int) = IntLiteral(n - m)
   def *(m: Int) = IntLiteral(n * m)
   def /(m: Int) = Div(this, IntLiteral(m))
   override lazy val toString = n.toString()
+  override val equalityDefiningMembers: BigInt = n
+}
+object IntLiteral extends CondFlyweightFactory[BigInt, IntLiteral, IntLiteral] {
+  override def actualCreate(args: BigInt): IntLiteral = new IntLiteral(args)
 }
 
-case class Null() extends Term with Literal {
+case object Null extends Term with Literal {
   val sort = sorts.Ref
   override lazy val toString = "Null"
 }
@@ -449,15 +612,15 @@ sealed trait BooleanLiteral extends BooleanTerm with Literal {
 }
 
 object BooleanLiteral extends (Boolean => BooleanLiteral) {
-  def apply(b: Boolean): BooleanLiteral = if (b) True() else False()
+  def apply(b: Boolean): BooleanLiteral = if (b) True else False
 }
 
-case class True() extends BooleanLiteral {
+case object True extends BooleanLiteral {
   val value = true
   override lazy val toString = "True"
 }
 
-case class False() extends BooleanLiteral {
+case object False extends BooleanLiteral {
   val value = false
   override lazy val toString = "False"
 }
@@ -535,9 +698,9 @@ class Quantification private[terms] (val q: Quantifier, /* TODO: Rename */
                                      val isGlobal: Boolean,
                                      val weight: Option[Int])
     extends BooleanTerm
-       with StructuralEquality {
+       with ConditionalFlyweight[(Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int]), Quantification] {
 
-  val equalityDefiningMembers = q :: vars :: body :: triggers :: weight :: Nil
+  val equalityDefiningMembers = (q, vars, body, triggers, name, isGlobal, weight)
 
   def copy(q: Quantifier = q,
            vars: Seq[Var] = vars,
@@ -568,7 +731,7 @@ class Quantification private[terms] (val q: Quantifier, /* TODO: Rename */
 }
 
 object Quantification
-    extends ((Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int]) => Quantification) {
+    extends CondFlyweightTermFactory[(Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int]), Quantification] {
 
   private val qidCounter = new AtomicInteger()
 
@@ -613,17 +776,15 @@ object Quantification
     /* TODO: If we optimise away a quantifier, we cannot, for example, access
      *       autoTrigger on the returned object.
      */
-    new Quantification(q, vars, tBody, triggers, name, isGlobal, weight)
+    createIfNonExistent(q, vars, tBody, triggers, name, isGlobal, weight)
 //    tBody match {
-//    case True() | False() => tBody
+//    case True | False => tBody
 //    case _ => new Quantification(q, vars, tBody, triggers)
 //  }
   }
 
-  def unapply(q: Quantification)
-             : Some[(Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int])] = {
-
-    Some((q.q, q.vars, q.body, q.triggers, q.name, q.isGlobal, q.weight))
+  override def actualCreate(args: (Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int])): Quantification = {
+    new Quantification(args._1, args._2, args._3, args._4, args._5, args._6, args._7)
   }
 }
 
@@ -634,83 +795,92 @@ sealed abstract class ArithmeticTerm extends Term {
 }
 
 class Plus(val p0: Term, val p1: Term) extends ArithmeticTerm
-    with BinaryOp[Term] with StructuralEqualityBinaryOp[Term] {
+    with ConditionalFlyweightBinaryOp[Plus] {
 
   override val op = "+"
 }
 
-object Plus extends ((Term, Term) => Term) {
+object Plus extends CondFlyweightTermFactory[(Term, Term), Plus] {
   import predef.Zero
 
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
+  override def apply(v0: (Term, Term)) = v0 match {
     case (t0, Zero) => t0
     case (Zero, t1) => t1
     case (IntLiteral(n0), IntLiteral(n1)) => IntLiteral(n0 + n1)
-    case _ => new Plus(e0, e1)
+    case (e0, e1) => createIfNonExistent(e0, e1)
   }
 
-  def unapply(t: Plus) = Some((t.p0, t.p1))
+  override def actualCreate(args: (Term, Term)): Plus = new Plus(args._1, args._2)
 }
 
 class Minus(val p0: Term, val p1: Term) extends ArithmeticTerm
-    with BinaryOp[Term] with StructuralEqualityBinaryOp[Term] {
+  with ConditionalFlyweightBinaryOp[Minus] {
 
   override val op = "-"
 }
 
-object Minus extends ((Term, Term) => Term) {
+object Minus extends CondFlyweightTermFactory[(Term, Term), Minus] {
   import predef.Zero
 
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
+  override def apply(v1: (Term, Term)) = v1 match {
     case (t0, Zero) => t0
     case (IntLiteral(n0), IntLiteral(n1)) => IntLiteral(n0 - n1)
     case (t0, t1) if t0 == t1 => Zero
-    case _ => new Minus(e0, e1)
+    case (e0, e1) => createIfNonExistent(e0, e1)
   }
 
-  def unapply(t: Minus) = Some((t.p0, t.p1))
+  override def actualCreate(args: (Term, Term)): Minus = new Minus(args._1, args._2)
 }
 
 class Times(val p0: Term, val p1: Term) extends ArithmeticTerm
-    with BinaryOp[Term] with StructuralEqualityBinaryOp[Term] {
+    with ConditionalFlyweightBinaryOp[Times] {
 
   override val op = "*"
 }
 
-object Times extends ((Term, Term) => Term) {
+object Times extends CondFlyweightTermFactory[(Term, Term), Times] {
   import predef.{Zero, One}
 
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
+  override def apply(v0: (Term, Term)) =v0 match {
     case (_, Zero) => Zero
     case (Zero, _) => Zero
     case (t0, One) => t0
     case (One, t1) => t1
     case (IntLiteral(n0), IntLiteral(n1)) => IntLiteral(n0 * n1)
-    case _ => new Times(e0, e1)
+    case (e0, e1) => createIfNonExistent(e0, e1)
   }
 
-  def unapply(t: Times) = Some((t.p0, t.p1))
+  override def actualCreate(args: (Term, Term)): Times = new Times(args._1, args._2)
 }
 
-case class Div(p0: Term, p1: Term) extends ArithmeticTerm
-    with BinaryOp[Term] {
+class Div(val p0: Term, val p1: Term) extends ArithmeticTerm
+    with ConditionalFlyweightBinaryOp[Div] {
 
   override val op = "/"
 }
 
-case class Mod(p0: Term, p1: Term) extends ArithmeticTerm
-    with BinaryOp[Term] {
+object Div extends CondFlyweightFactory[(Term, Term), Div, Div] {
+  override def actualCreate(args: (Term, Term)): Div = new Div(args._1, args._2)
+}
+
+class Mod(val p0: Term, val p1: Term) extends ArithmeticTerm
+    with ConditionalFlyweightBinaryOp[Mod] {
 
   override val op = "%"
 }
 
+object Mod extends CondFlyweightFactory[(Term, Term), Mod, Mod] {
+  override def actualCreate(args: (Term, Term)): Mod = new Mod(args._1, args._2)
+}
+
+
 /* Boolean expression terms */
 
 sealed trait BooleanTerm extends Term { override val sort = sorts.Bool }
 
 class Not(val p: Term) extends BooleanTerm
-    with StructuralEqualityUnaryOp[Term] {
-
+    with ConditionalFlyweightUnaryOp[Not] {
+  assert(p.sort == sorts.Bool)
   override val op = "!"
 
   override lazy val toString = p match {
@@ -719,19 +889,19 @@ class Not(val p: Term) extends BooleanTerm
   }
 }
 
-object Not extends (Term => Term) {
-  def apply(e0: Term) = e0 match {
+object Not extends CondFlyweightTermFactory[Term, Not] {
+
+  override def apply(e0: Term) = e0 match {
     case Not(e1) => e1
-    case True() => False()
-    case False() => True()
-    case _ => new Not(e0)
+    case True => False
+    case False => True
+    case _ => createIfNonExistent(e0)
   }
-
-  def unapply(e: Not) = Some(e.p)
+  override def actualCreate(args: Term): Not = new Not(args)
 }
 
-class Or(val ts: Seq[Term]) extends BooleanTerm
-    with StructuralEquality {
+class Or private[terms] (val ts: Seq[Term]) extends BooleanTerm
+    with ConditionalFlyweight[Seq[Term], Or] {
 
   assert(ts.nonEmpty, "Expected at least one term, but found none")
 
@@ -746,14 +916,16 @@ class Or(val ts: Seq[Term]) extends BooleanTerm
  *       that conflicts with using extractor objects to simplify terms,
  *       since extractor objects can't be type-parametrised.
  */
-object Or extends (Iterable[Term] => Term) {
+object Or extends GeneralCondFlyweightFactory[Iterable[Term], Seq[Term], Term, Or] {
   def apply(ts: Term*) = createOr(ts)
   def apply(ts: Iterable[Term]) = createOr(ts.toSeq)
 
+
+
   //  def apply(e0: Term, e1: Term) = (e0, e1) match {
-  //    case (True(), _) | (_, True()) => True()
-  //    case (False(), _) => e1
-  //    case (_, False()) => e0
+  //    case (True, _) | (_, True) => True
+  //    case (False, _) => e1
+  //    case (_, False) => e0
   //    case _ if e0 == e1 => e0
   //    case _ => new Or(e0, e1)
   //  }
@@ -761,22 +933,22 @@ object Or extends (Iterable[Term] => Term) {
   @inline
   def createOr(_ts: Seq[Term]): Term = {
     var ts = _ts.flatMap { case Or(ts1) => ts1; case other => other :: Nil}
-    ts = _ts.filterNot(_ == False())
+    ts = _ts.filterNot(_ == False)
     ts = ts.distinct
 
     ts match {
-      case Seq() => False()
+      case Seq() => False
       case Seq(t) => t
-      case _ if ts.contains(True()) => True()
-      case _ => new Or(ts)
+      case _ if ts.contains(True) => True
+      case _ => createIfNonExistent(ts)
     }
   }
 
-  def unapply(e: Or) = Some(e.ts)
+  override def actualCreate(args: Seq[Term]): Or = new Or(args)
 }
 
-class And(val ts: Seq[Term]) extends BooleanTerm
-    with StructuralEquality {
+class And private[terms](val ts: Seq[Term]) extends BooleanTerm
+    with ConditionalFlyweight[Seq[Term], And] {
 
   assert(ts.nonEmpty, "Expected at least one term, but found none")
 
@@ -785,86 +957,86 @@ class And(val ts: Seq[Term]) extends BooleanTerm
   override lazy val toString = ts.mkString(" && ")
 }
 
-object And extends (Iterable[Term] => Term) {
+object And extends GeneralCondFlyweightFactory[Iterable[Term], Seq[Term], Term, And] {
   def apply(ts: Term*) = createAnd(ts)
   def apply(ts: Iterable[Term]) = createAnd(ts.toSeq)
 
   @inline
   def createAnd(_ts: Seq[Term]): Term = {
     var ts = _ts.flatMap { case And(ts1) => ts1; case other => other :: Nil}
-    ts = _ts.filterNot(_ == True())
+    ts = _ts.filterNot(_ == True)
     ts = ts.distinct
 
     ts match {
-      case Seq() => True()
+      case Seq() => True
       case Seq(t) => t
-      case _ if ts.contains(False()) => False()
-      case _ => new And(ts)
+      case _ if ts.contains(False) => False
+      case _ => createIfNonExistent(ts)
     }
   }
 
-  def unapply(e: And) = Some(e.ts)
+  override def actualCreate(args: Seq[Term]): And = new And(args)
 }
 
 class Implies(val p0: Term, val p1: Term) extends BooleanTerm
-    with StructuralEqualityBinaryOp[Term] {
+    with ConditionalFlyweightBinaryOp[Implies] {
 
   override val op = "==>"
 }
 
-object Implies extends ((Term, Term) => Term) {
+object Implies extends CondFlyweightTermFactory[(Term, Term), Implies] {
   @tailrec
-  def apply(e0: Term, e1: Term): Term = (e0, e1) match {
-    case (True(), _) => e1
-    case (False(), _) => True()
-    case (_, True()) => True()
-    case (_, Implies(e10, e11)) => Implies(And(e0, e10), e11)
-    case _ if e0 == e1 => True()
-    case _ => new Implies(e0, e1)
+  override def apply(v0: (Term, Term)): Term = v0 match {
+    case (True, e1) => e1
+    case (False, _) => True
+    case (_, True) => True
+    case (e0, Implies(e10, e11)) => Implies(And(e0, e10), e11)
+    case (e0, e1) if e0 == e1 => True
+    case (e0, e1) => createIfNonExistent(e0, e1)
   }
 
-  def unapply(e: Implies) = Some((e.p0, e.p1))
+  override def actualCreate(args: (Term, Term)): Implies = new Implies(args._1, args._2)
 }
 
 class Iff(val p0: Term, val p1: Term) extends BooleanTerm
-    with StructuralEqualityBinaryOp[Term] {
+    with ConditionalFlyweightBinaryOp[Iff] {
 
   override val op = "<==>"
 }
 
-object Iff extends ((Term, Term) => Term) {
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
-    case (True(), _) => e1
-    case (_, True()) => e0
-    case _ if e0 == e1 => True()
-    case _ => new Iff(e0, e1)
+object Iff extends CondFlyweightTermFactory[(Term, Term), Iff] {
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (True, e1) => e1
+    case (e0, True) => e0
+    case (e0, e1) if e0 == e1 => True
+    case (e0, e1) => createIfNonExistent(e0, e1)
   }
 
-  def unapply(e: Iff) = Some((e.p0, e.p1))
+  override def actualCreate(args: (Term, Term)): Iff = new Iff(args._1, args._2)
 }
 
-class Ite(val t0: Term, val t1: Term, val t2: Term)
-    extends Term with StructuralEquality {
+class Ite private[terms] (val t0: Term, val t1: Term, val t2: Term)
+    extends Term with ConditionalFlyweight[(Term, Term, Term), Ite] {
 
   assert(t0.sort == sorts.Bool && t1.sort == t2.sort, /* @elidable */
          s"Ite term Ite($t0, $t1, $t2) is not well-sorted: ${t0.sort}, ${t1.sort}, ${t2.sort}")
 
-  val equalityDefiningMembers = t0 :: t1 :: t2 :: Nil
+  val equalityDefiningMembers = (t0, t1, t2)
   val sort = t1.sort
   override lazy val toString = s"($t0 ? $t1 : $t2)"
 }
 
-object Ite extends ((Term, Term, Term) => Term) {
-  def apply(e0: Term, e1: Term, e2: Term) = (e0, e1, e2) match {
-    case _ if e1 == e2 => e1
-    case (True(), _, _) => e1
-    case (False(), _, _) => e2
-    case (_, True(), False()) => e0
-    case (_, False(), True()) => Not(e0)
-    case _ => new Ite(e0, e1, e2)
+object Ite extends CondFlyweightTermFactory[(Term, Term, Term), Ite] {
+  override def apply(v0: (Term, Term, Term)) = v0 match {
+    case (_, e1, e2) if e1 == e2 => e1
+    case (True, e1, _) => e1
+    case (False, _, e2) => e2
+    case (e0, True, False) => e0
+    case (e0, False, True) => Not(e0)
+    case _ => createIfNonExistent(v0)
   }
 
-  def unapply(e: Ite) = Some((e.t0, e.t1, e.t2))
+  override def actualCreate(args: (Term, Term, Term)): Ite = new Ite(args._1, args._2, args._3)
 }
 
 /* Comparison expression terms */
@@ -881,7 +1053,7 @@ object Equals extends ((Term, Term) => BooleanTerm) {
     // Note that the syntactic simplifications (first two cases) can interfere with triggering
     // if they eliminate potential trigger terms.
     (e0, e1) match {
-      case (`e0`, `e0`) => True()
+      case (`e0`, `e0`) => True
       case (l1: Literal, l2: Literal) => BooleanLiteral(l1 == l2)
       case _ =>
         e0.sort match {
@@ -903,10 +1075,10 @@ object Equals extends ((Term, Term) => BooleanTerm) {
               case _ => /* Ok */
             }
 
-            new BuiltinEquals(e0, e1)
+            BuiltinEquals(e0, e1)
 
-          case _: sorts.Seq | _: sorts.Set | _: sorts.Multiset | _: sorts.Map => new CustomEquals(e0, e1)
-          case _ => new BuiltinEquals(e0, e1)
+          case _: sorts.Seq | _: sorts.Set | _: sorts.Multiset | _: sorts.Map => CustomEquals(e0, e1)
+          case _ => BuiltinEquals(e0, e1)
         }
     }
   }
@@ -915,35 +1087,32 @@ object Equals extends ((Term, Term) => BooleanTerm) {
 }
 
 /* Represents built-in equality, e.g., '=' in SMT-LIB */
-class BuiltinEquals private[terms] (val p0: Term, val p1: Term) extends Equals
-    with StructuralEqualityBinaryOp[Term]
+class BuiltinEquals private[terms] (val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[BuiltinEquals] with Equals
 
-object BuiltinEquals extends ((Term, Term) => BooleanTerm) {
-  def apply(t1: Term, t2: Term) = (t1, t2) match {
+object BuiltinEquals extends CondFlyweightFactory[(Term, Term), BooleanTerm, BuiltinEquals] {
+  override def apply(v0: (Term, Term)) = v0 match {
     case (p0: PermLiteral, p1: PermLiteral) =>
-      // NOTE: The else-case (False()) is only justified because permission literals are stored in a normal form
+      // NOTE: The else-case (False) is only justified because permission literals are stored in a normal form
       // such that two literals are semantically equivalent iff they are syntactically equivalent.
-      if (p0.literal == p1.literal) True() else False()
-    case _ => new BuiltinEquals(t1, t2)
+      if (p0.literal == p1.literal) True else False
+    case _ => createIfNonExistent(v0)
   }
 
-  def unapply(e: BuiltinEquals) = Some((e.p0, e.p1))
+  override def actualCreate(args: (Term, Term)): BuiltinEquals = new BuiltinEquals(args._1, args._2)
 }
 
 /* Custom equality that (potentially) needs to be axiomatised. */
-class CustomEquals private[terms] (val p0: Term, val p1: Term) extends Equals
-    with StructuralEqualityBinaryOp[Term] {
+class CustomEquals private[terms] (val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[CustomEquals] with Equals {
 
   override val op = "==="
 }
 
-object CustomEquals extends ((Term, Term) => BooleanTerm) {
-  def apply(t1: Term, t2: Term) = new CustomEquals(t1, t2)
-  def unapply(e: CustomEquals) = Some((e.p0, e.p1))
+object CustomEquals extends CondFlyweightFactory[(Term, Term), BooleanTerm, CustomEquals] {
+  override def actualCreate(args: (Term, Term)): CustomEquals = new CustomEquals(args._1, args._2)
 }
 
-class Less(val p0: Term, val p1: Term) extends ComparisonTerm
-    with StructuralEqualityBinaryOp[Term] {
+class Less private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm
+    with ConditionalFlyweightBinaryOp[Less] {
 
   assert(p0.sort == p1.sort,
          s"Expected both operands to be of the same sort, but found ${p0.sort} ($p0) and ${p1.sort} ($p1).")
@@ -951,66 +1120,66 @@ class Less(val p0: Term, val p1: Term) extends ComparisonTerm
   override val op = "<"
 }
 
-object Less extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) {
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
-    case (IntLiteral(n0), IntLiteral(n1)) => if (n0 < n1) True() else False()
-    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal < pl1.literal) True() else False()
-    case (t0, t1) if t0 == t1 => False()
-    case _ => new Less(e0, e1)
+object Less extends /* OptimisingBinaryArithmeticOperation with */ CondFlyweightTermFactory[(Term, Term), Less] {
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (IntLiteral(n0), IntLiteral(n1)) => if (n0 < n1) True else False
+    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal < pl1.literal) True else False
+    case (t0, t1) if t0 == t1 => False
+    case _ => createIfNonExistent(v0)
   }
 
-  def unapply(e: Less) = Some((e.p0, e.p1))
+  override def actualCreate(args: (Term, Term)): Less = new Less(args._1, args._2)
 }
 
-class AtMost(val p0: Term, val p1: Term) extends ComparisonTerm
-    with StructuralEqualityBinaryOp[Term] {
+class AtMost private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm
+    with ConditionalFlyweightBinaryOp[AtMost] {
 
   override val op = "<="
 }
 
-object AtMost extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) {
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
-    case (IntLiteral(n0), IntLiteral(n1)) => if (n0 <= n1) True() else False()
-    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal <= pl1.literal) True() else False()
-    case (t0, t1) if t0 == t1 => True()
-    case _ => new AtMost(e0, e1)
+object AtMost extends /* OptimisingBinaryArithmeticOperation with */ CondFlyweightTermFactory[(Term, Term), AtMost] {
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (IntLiteral(n0), IntLiteral(n1)) => if (n0 <= n1) True else False
+    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal <= pl1.literal) True else False
+    case (t0, t1) if t0 == t1 => True
+    case _ => createIfNonExistent(v0)
   }
 
-  def unapply(e: AtMost) = Some((e.p0, e.p1))
+  override def actualCreate(args: (Term, Term)): AtMost = new AtMost(args._1, args._2)
 }
 
-class Greater(val p0: Term, val p1: Term) extends ComparisonTerm
-    with StructuralEqualityBinaryOp[Term] {
+class Greater private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm
+    with ConditionalFlyweightBinaryOp[Greater] {
 
   override val op = ">"
 }
 
-object Greater extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) {
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
-    case (IntLiteral(n0), IntLiteral(n1)) => if (n0 > n1) True() else False()
-    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal > pl1.literal) True() else False()
-    case (t0, t1) if t0 == t1 => False()
-    case _ => new Greater(e0, e1)
+object Greater extends /* OptimisingBinaryArithmeticOperation with */ CondFlyweightTermFactory[(Term, Term), Greater] {
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (IntLiteral(n0), IntLiteral(n1)) => if (n0 > n1) True else False
+    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal > pl1.literal) True else False
+    case (t0, t1) if t0 == t1 => False
+    case _ => createIfNonExistent(v0)
   }
 
-  def unapply(e: Greater) = Some((e.p0, e.p1))
+  override def actualCreate(args: (Term, Term)): Greater = new Greater(args._1, args._2)
 }
 
-class AtLeast(val p0: Term, val p1: Term) extends ComparisonTerm
-    with StructuralEqualityBinaryOp[Term] {
+class AtLeast private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm
+    with ConditionalFlyweightBinaryOp[AtLeast] {
 
   override val op = ">="
 }
 
-object AtLeast extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) {
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
-    case (IntLiteral(n0), IntLiteral(n1)) => if (n0 >= n1) True() else False()
-    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal >= pl1.literal) True() else False()
-    case (t0, t1) if t0 == t1 => True()
-    case _ => new AtLeast(e0, e1)
+object AtLeast extends /* OptimisingBinaryArithmeticOperation with */ CondFlyweightTermFactory[(Term, Term), AtLeast] {
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (IntLiteral(n0), IntLiteral(n1)) => if (n0 >= n1) True else False
+    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal >= pl1.literal) True else False
+    case (t0, t1) if t0 == t1 => True
+    case _ => createIfNonExistent(v0)
   }
 
-  def unapply(e: AtLeast) = Some((e.p0, e.p1))
+  override def actualCreate(args: (Term, Term)): AtLeast = new AtLeast(args._1, args._2)
 }
 
 /*
@@ -1045,6 +1214,8 @@ final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] {
     case _ => false
   }
 
+  override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(n, d)
+
   override lazy val toString = s"$numerator/$denominator"
 }
 
@@ -1066,133 +1237,136 @@ sealed trait Permissions extends Term {
 
 sealed abstract class PermLiteral(val literal: Rational) extends Permissions
 
-case class NoPerm() extends PermLiteral(Rational.zero) { override lazy val toString = "Z" }
-case class FullPerm() extends PermLiteral(Rational.one) { override lazy val toString = "W" }
+case object NoPerm extends PermLiteral(Rational.zero) { override lazy val toString = "Z" }
+case object FullPerm extends PermLiteral(Rational.one) { override lazy val toString = "W" }
 
-class FractionPermLiteral(r: Rational) extends PermLiteral(r) {
-  override def equals(obj: Any) = obj match {
-    case p: FractionPermLiteral => literal == p.literal
-    case _ => false
-  }
+class FractionPermLiteral private[terms] (r: Rational) extends PermLiteral(r) with ConditionalFlyweight[Rational, FractionPermLiteral] {
+  override val equalityDefiningMembers: Rational = r
   override lazy val toString = literal.toString
 }
 
-object FractionPermLiteral extends (Rational => Permissions) {
-  def apply(r: Rational) = r match {
-    case Rational(n, _) if n == 0 => NoPerm()
-    case Rational(n, d) if n == d => FullPerm()
-    case _ => new FractionPermLiteral(r)
+object FractionPermLiteral extends CondFlyweightFactory[Rational, Permissions, FractionPermLiteral] {
+  override def apply(r: Rational) = r match {
+    case Rational(n, _) if n == 0 => NoPerm
+    case Rational(n, d) if n == d => FullPerm
+    case _ => createIfNonExistent(r)
   }
 
-  def unapply(t: FractionPermLiteral) = Some(t.literal)
+  override def actualCreate(args: Rational): FractionPermLiteral = new FractionPermLiteral(args)
 }
 
-class FractionPerm(val n: Term, val d: Term)
+class FractionPerm private[terms] (val n: Term, val d: Term)
     extends Permissions
-       with StructuralEquality {
+       with ConditionalFlyweight[(Term, Term), FractionPerm] {
 
-  val equalityDefiningMembers = n :: d :: Nil
+  val equalityDefiningMembers = (n, d)
   override lazy val toString = s"$n/$d"
 }
 
-object FractionPerm extends ((Term, Term) => Permissions) {
-  def apply(n: Term, d: Term) = (n, d) match {
+object FractionPerm extends CondFlyweightFactory[(Term, Term), Permissions, FractionPerm] {
+  override def apply(v: (Term, Term)) = v match {
     case (IntLiteral(i1), IntLiteral(i2)) if i2 != 0 => FractionPermLiteral(Rational(i1, i2))
-    case _ => new FractionPerm(n, d)
+    case _ => createIfNonExistent(v)
   }
 
-  def unapply(fp: FractionPerm) = Some((fp.n, fp.d))
+  override def actualCreate(args: (Term, Term)): FractionPerm = new FractionPerm(args._1, args._2)
 }
 
-case class IsValidPermVar(v: Var) extends BooleanTerm {
+class IsValidPermVar private[terms] (val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsValidPermVar] {
+  override val equalityDefiningMembers: Var = v
   override lazy val toString = s"PVar($v)"
 }
 
-case class IsReadPermVar(v: Var) extends BooleanTerm {
+object IsValidPermVar extends CondFlyweightTermFactory[Var, IsValidPermVar] {
+  override def actualCreate(args: Var): IsValidPermVar = new IsValidPermVar((args))
+}
+
+class IsReadPermVar private[terms] (val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsReadPermVar] {
+  override val equalityDefiningMembers: Var = v
   override lazy val toString = s"RdVar($v)"
 }
 
-class PermTimes(val p0: Term, val p1: Term)
+object IsReadPermVar extends CondFlyweightTermFactory[Var, IsReadPermVar] {
+  override def actualCreate(args: Var): IsReadPermVar = new IsReadPermVar((args))
+}
+
+class PermTimes private[terms] (val p0: Term, val p1: Term)
     extends Permissions
-       with StructuralEqualityBinaryOp[Term] {
+       with ConditionalFlyweightBinaryOp[PermTimes] {
 
   override val op = "*"
 }
 
-object PermTimes extends ((Term, Term) => Term) {
-  def apply(t0: Term, t1: Term) = (t0, t1) match {
-    case (FullPerm(), t) => t
-    case (t, FullPerm()) => t
-    case (NoPerm(), _) => NoPerm()
-    case (_, NoPerm()) => NoPerm()
+object PermTimes extends CondFlyweightTermFactory[(Term, Term), PermTimes] {
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (FullPerm, t) => t
+    case (t, FullPerm) => t
+    case (NoPerm, _) => NoPerm
+    case (_, NoPerm) => NoPerm
     case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal * p1.literal)
-    case (_, _) => new PermTimes(t0, t1)
+    case (_, _) => createIfNonExistent(v0)
   }
 
-  def unapply(pt: PermTimes) = Some((pt.p0, pt.p1))
+  override def actualCreate(args: (Term, Term)): PermTimes = new PermTimes(args._1, args._2)
 }
 
-class IntPermTimes(val p0: Term, val p1: Term)
-    extends Permissions
-       with BinaryOp[Term]
-       with StructuralEqualityBinaryOp[Term] {
+class IntPermTimes private[terms] (val p0: Term, val p1: Term)
+    extends ConditionalFlyweightBinaryOp[IntPermTimes]
+      with Permissions
+      with BinaryOp[Term] {
 
   override val op = "*"
 }
 
-object IntPermTimes extends ((Term, Term) => Term) {
+object IntPermTimes extends CondFlyweightTermFactory[(Term, Term), IntPermTimes] {
   import predef.{Zero, One}
 
-  def apply(t0: Term, t1: Term) = (t0, t1) match {
-    case (Zero, _) => NoPerm()
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (Zero, _) => NoPerm
     case (One, t) => t
-    case (_, NoPerm()) => NoPerm()
+    case (_, NoPerm) => NoPerm
     case (IntLiteral(i), p: PermLiteral) => FractionPermLiteral(Rational(i, 1) * p.literal)
-    case (_, _) => new IntPermTimes(t0, t1)
+    case (_, _) => createIfNonExistent(v0)
   }
 
-  def unapply(pt: IntPermTimes) = Some((pt.p0, pt.p1))
+  override def actualCreate(args: (Term, Term)): IntPermTimes = new IntPermTimes(args._1, args._2)
 }
 
-class PermIntDiv(val p0: Term, val p1: Term)
-    extends Permissions
-       with BinaryOp[Term]
-       with StructuralEqualityBinaryOp[Term] {
+class PermIntDiv private[terms] (val p0: Term, val p1: Term)
+    extends ConditionalFlyweightBinaryOp[PermIntDiv]
+      with Permissions
+      with BinaryOp[Term] {
 
   utils.assertSort(p1, "Second term", sorts.Int)
 
   override val op = "/"
 }
 
-object PermIntDiv extends ((Term, Term) => Term) {
+object PermIntDiv extends CondFlyweightTermFactory[(Term, Term), PermIntDiv] {
   import predef.One
 
-  def apply(t0: Term, t1: Term) = (t0, t1) match {
+  override def apply(v0: (Term, Term)) = v0 match {
     case (t, One) => t
     case (p: PermLiteral, IntLiteral(i)) if i != 0 => FractionPermLiteral(p.literal / Rational(i, 1))
-    case (_, _) => new PermIntDiv(t0, t1)
+    case (_, _) => createIfNonExistent(v0)
   }
 
-  def unapply(t: PermIntDiv) = Some((t.p0, t.p1))
+  override def actualCreate(args: (Term, Term)): PermIntDiv = new PermIntDiv(args._1, args._2)
 }
 
-class PermPermDiv(val p0: Term, val p1: Term)
-  extends Permissions
-    with BinaryOp[Term]
-    with StructuralEqualityBinaryOp[Term] {
+class PermPermDiv private[terms] (val p0: Term, val p1: Term)
+  extends ConditionalFlyweightBinaryOp[PermPermDiv]
+    with Permissions
+    with BinaryOp[Term] {
 
   utils.assertSort(p1, "Second term", sorts.Perm)
 
   override val op = "/"
 }
 
-object PermPermDiv extends ((Term, Term) => Term) {
+object PermPermDiv extends CondFlyweightTermFactory[(Term, Term), PermPermDiv] {
 
-  def apply(t0: Term, t1: Term) = (t0, t1) match {
-    case (_, _) => new PermPermDiv(t0, t1)
-  }
-
-  def unapply(t: PermPermDiv) = Some((t.p0, t.p1))
+  override def actualCreate(args: (Term, Term)): PermPermDiv = new PermPermDiv(args._1, args._2)
 }
 
 object PermDiv extends ((Term, Term) => Term) {
@@ -1201,33 +1375,33 @@ object PermDiv extends ((Term, Term) => Term) {
   def apply(t0: Term, t1: Term) = PermTimes(t0, FractionPerm(One, t1))
 }
 
-class PermPlus(val p0: Term, val p1: Term)
-    extends Permissions
-       with BinaryOp[Term]
-       with StructuralEqualityBinaryOp[Term] {
+class PermPlus private[terms] (val p0: Term, val p1: Term)
+    extends ConditionalFlyweightBinaryOp[PermPlus]
+      with Permissions
+      with BinaryOp[Term] {
 
   override val op = "+"
 }
 
-object PermPlus extends ((Term, Term) => Term) {
-  def apply(t0: Term, t1: Term) = (t0, t1) match {
-    case (NoPerm(), _) => t1
-    case (_, NoPerm()) => t0
+object PermPlus extends CondFlyweightTermFactory[(Term, Term), PermPlus] {
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (NoPerm, t1) => t1
+    case (t0, NoPerm) => t0
     case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal + p1.literal)
     case (FractionPerm(n1, d1), FractionPerm(n2, d2)) if d1 == d2 => FractionPerm(Plus(n1, n2), d1)
-    case (PermMinus(t00, t01), _) if t01 == t1 => t00
-    case (_, PermMinus(t10, t11)) if t11 == t0 => t10
+    case (PermMinus(t00, t01), t1) if t01 == t1 => t00
+    case (t0, PermMinus(t10, t11)) if t11 == t0 => t10
 
-    case (_, _) => new PermPlus(t0, t1)
+    case (_, _) => createIfNonExistent(v0)
   }
 
-  def unapply(pp: PermPlus) = Some((pp.p0, pp.p1))
+  override def actualCreate(args: (Term, Term)): PermPlus = new PermPlus(args._1, args._2)
 }
 
-class PermMinus(val p0: Term, val p1: Term)
+class PermMinus private[terms] (val p0: Term, val p1: Term)
     extends Permissions
        with BinaryOp[Term]
-       with StructuralEqualityBinaryOp[Term] {
+       with ConditionalFlyweightBinaryOp[PermMinus] {
 
   override val op = "-"
 
@@ -1237,68 +1411,68 @@ class PermMinus(val p0: Term, val p1: Term)
   }
 }
 
-object PermMinus extends ((Term, Term) => Term) {
-  def apply(t0: Term, t1: Term) = (t0, t1) match {
-    case (_, NoPerm()) => t0
-    case (p0, p1) if p0 == p1 => NoPerm()
+object PermMinus extends CondFlyweightTermFactory[(Term, Term), PermMinus] {
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (t0, NoPerm) => t0
+    case (p0, p1) if p0 == p1 => NoPerm
     case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal - p1.literal)
     case (p0, PermMinus(p1, p2)) if p0 == p1 => p2
     case (PermPlus(p0, p1), p2) if p0 == p2 => p1
     case (PermPlus(p0, p1), p2) if p1 == p2 => p0
-    case (_, _) => new PermMinus(t0, t1)
+    case (_, _) => createIfNonExistent(v0)
   }
 
-  def unapply(pm: PermMinus) = Some((pm.p0, pm.p1))
+  override def actualCreate(args: (Term, Term)): PermMinus = new PermMinus(args._1, args._2)
 }
 
-class PermLess(val p0: Term, val p1: Term)
+class PermLess private[terms] (val p0: Term, val p1: Term)
     extends BooleanTerm
        with BinaryOp[Term]
-       with StructuralEqualityBinaryOp[Term] {
+       with ConditionalFlyweightBinaryOp[PermLess] {
 
   override lazy val toString = s"($p0) < ($p1)"
 
   override val op = "<"
 }
 
-object PermLess extends ((Term, Term) => Term) {
-  def apply(t0: Term, t1: Term): Term = {
-    (t0, t1) match {
-      case _ if t0 == t1 => False()
-      case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal < p1.literal) True() else False()
+object PermLess extends CondFlyweightTermFactory[(Term, Term), PermLess] {
+  override def apply(v0: (Term, Term)): Term = {
+    v0 match {
+      case (t0, t1) if t0 == t1 => False
+      case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal < p1.literal) True else False
 
-      case (`t0`, Ite(tCond, tIf, tElse)) =>
+      case (t0, Ite(tCond, tIf, tElse)) =>
         /* The pattern p0 < b ? p1 : p2 arises very often in the context of quantified permissions.
          * Pushing the comparisons into the ite allows further simplifications.
          */
         Ite(tCond, PermLess(t0, tIf), PermLess(t0, tElse))
 
-      case _ => new PermLess(t0, t1)
+      case _ => createIfNonExistent(v0)
     }
   }
 
-  def unapply(pl: PermLess) = Some((pl.p0, pl.p1))
+  override def actualCreate(args: (Term, Term)): PermLess = new PermLess(args._1, args._2)
 }
 
-class PermAtMost(val p0: Term, val p1: Term) extends ComparisonTerm
-    with StructuralEqualityBinaryOp[Term] {
+class PermAtMost private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm
+    with ConditionalFlyweightBinaryOp[PermAtMost] {
 
   override val op = "<="
 }
 
-object PermAtMost extends ((Term, Term) => Term) {
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
-    case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal <= p1.literal) True() else False()
-    case (t0, t1) if t0 == t1 => True()
-    case _ => new PermAtMost(e0, e1)
+object PermAtMost extends CondFlyweightTermFactory[(Term, Term), PermAtMost] {
+  override def apply(v0: (Term, Term)) = v0 match {
+    case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal <= p1.literal) True else False
+    case (t0, t1) if t0 == t1 => True
+    case _ => createIfNonExistent(v0)
   }
 
-  def unapply(e: PermAtMost) = Some((e.p0, e.p1))
+  override def actualCreate(args: (Term, Term)): PermAtMost = new PermAtMost(args._1, args._2)
 }
 
-class PermMin(val p0: Term, val p1: Term) extends Permissions
+class PermMin private[terms] (val p0: Term, val p1: Term) extends Permissions
     with BinaryOp[Term]
-    with StructuralEqualityBinaryOp[Term] {
+    with ConditionalFlyweightBinaryOp[PermMin] {
 
   utils.assertSort(p0, "Permission 1st", sorts.Perm)
   utils.assertSort(p1, "Permission 2nd", sorts.Perm)
@@ -1306,14 +1480,14 @@ class PermMin(val p0: Term, val p1: Term) extends Permissions
   override lazy val toString = s"min ($p0, $p1)"
 }
 
-object PermMin extends ((Term, Term) => Term) {
-  def apply(e0: Term, e1: Term) = (e0, e1) match {
+object PermMin extends CondFlyweightTermFactory[(Term, Term), PermMin] {
+  override def apply(v0: (Term, Term)) = v0 match {
     case (t0, t1) if t0 == t1 => t0
     case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal > p1.literal) p1 else p0
-    case _ => new PermMin(e0, e1)
+    case _ => createIfNonExistent(v0)
   }
 
-  def unapply(e: PermMin) = Some((e.p0, e.p1))
+  override def actualCreate(args: (Term, Term)): PermMin = new PermMin(args._1, args._2)
 }
 
 /* Sequences */
@@ -1323,30 +1497,47 @@ sealed trait SeqTerm extends Term {
   val sort: sorts.Seq
 }
 
-case class SeqRanged(p0: Term, p1: Term) extends SeqTerm /* with BinaryOp[Term] */ {
+class SeqRanged private[terms] (val p0: Term, val p1: Term) extends SeqTerm /* with BinaryOp[Term] */
+  with ConditionalFlyweight[(Term, Term), SeqRanged] {
   utils.assertSort(p0, "first operand", sorts.Int)
   utils.assertSort(p1, "second operand", sorts.Int)
 
   val elementsSort = sorts.Int
   val sort = sorts.Seq(elementsSort)
 
+  override val equalityDefiningMembers: (Term, Term) = (p0, p1)
+
   override lazy val toString = s"[$p0..$p1]"
 }
 
-case class SeqNil(elementsSort: Sort) extends SeqTerm with Literal {
+object SeqRanged extends CondFlyweightTermFactory[(Term, Term), SeqRanged] {
+  override def actualCreate(args: (Term, Term)): SeqRanged = new SeqRanged(args._1, args._2)
+}
+
+class SeqNil private[terms] (val elementsSort: Sort) extends SeqTerm with Literal with ConditionalFlyweight[Sort, SeqNil] {
   val sort = sorts.Seq(elementsSort)
   override lazy val toString = "Nil"
+  override val equalityDefiningMembers: Sort = elementsSort
+}
+
+object SeqNil extends CondFlyweightTermFactory[Sort, SeqNil] {
+  override def actualCreate(args: Sort): SeqNil = new SeqNil(args)
 }
 
-case class SeqSingleton(p: Term) extends SeqTerm /* with UnaryOp[Term] */ {
+class SeqSingleton private[terms] (val p: Term) extends SeqTerm /* with UnaryOp[Term] */ with ConditionalFlyweight[Term, SeqSingleton] {
   val elementsSort = p.sort
   val sort = sorts.Seq(elementsSort)
+  override val equalityDefiningMembers: Term = p
 
   override lazy val toString = s"[$p]"
 }
 
-class SeqAppend(val p0: Term, val p1: Term) extends SeqTerm
-    with StructuralEqualityBinaryOp[Term] {
+object SeqSingleton extends CondFlyweightFactory[Term, SeqTerm, SeqSingleton] {
+  override def actualCreate(args: Term): SeqSingleton = new SeqSingleton(args)
+}
+
+class SeqAppend private[terms] (val p0: Term, val p1: Term) extends SeqTerm
+    with ConditionalFlyweightBinaryOp[SeqAppend] {
 
   val elementsSort = p0.sort.asInstanceOf[sorts.Seq].elementsSort
   val sort = sorts.Seq(elementsSort)
@@ -1354,17 +1545,17 @@ class SeqAppend(val p0: Term, val p1: Term) extends SeqTerm
   override val op = "++"
 }
 
-object SeqAppend extends ((Term, Term) => SeqTerm) {
-  def apply(t0: Term, t1: Term) = {
-    utils.assertSameSorts[sorts.Seq](t0, t1)
-    new SeqAppend(t0, t1)
+object SeqAppend extends CondFlyweightTermFactory[(Term, Term), SeqAppend] {
+  override def apply(v0: (Term, Term)) = {
+    utils.assertSameSorts[sorts.Seq](v0._1, v0._2)
+    createIfNonExistent(v0)
   }
 
-  def unapply(sa: SeqAppend) = Some((sa.p0, sa.p1))
+  override def actualCreate(args: (Term, Term)): SeqAppend = new SeqAppend(args._1, args._2)
 }
 
-class SeqDrop(val p0: Term, val p1: Term) extends SeqTerm
-    with StructuralEqualityBinaryOp[Term] {
+class SeqDrop private[terms] (val p0: Term, val p1: Term) extends SeqTerm
+    with ConditionalFlyweightBinaryOp[SeqDrop] {
 
   val elementsSort = p0.sort.asInstanceOf[sorts.Seq].elementsSort
   val sort = sorts.Seq(elementsSort)
@@ -1372,18 +1563,19 @@ class SeqDrop(val p0: Term, val p1: Term) extends SeqTerm
   override lazy val toString = p0.toString + "[" + p1.toString + ":]"
 }
 
-object SeqDrop extends ((Term, Term) => SeqTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SeqDrop extends CondFlyweightTermFactory[(Term, Term), SeqDrop] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq])
     utils.assertSort(t1, "second operand", sorts.Int)
-    new SeqDrop(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(sd: SeqDrop) = Some((sd.p0, sd.p1))
+  override def actualCreate(args: (Term, Term)): SeqDrop = new SeqDrop(args._1, args._2)
 }
 
-class SeqTake(val p0: Term, val p1: Term) extends SeqTerm
-    with StructuralEqualityBinaryOp[Term] {
+class SeqTake private[terms] (val p0: Term, val p1: Term) extends SeqTerm
+    with ConditionalFlyweightBinaryOp[SeqTake] {
 
   val elementsSort = p0.sort.asInstanceOf[sorts.Seq].elementsSort
   val sort = sorts.Seq(elementsSort)
@@ -1391,86 +1583,90 @@ class SeqTake(val p0: Term, val p1: Term) extends SeqTerm
   override lazy val toString = p0.toString + "[:" + p1.toString + "]"
 }
 
-object SeqTake extends ((Term, Term) => SeqTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SeqTake extends CondFlyweightTermFactory[(Term, Term), SeqTake] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq])
     utils.assertSort(t1, "second operand", sorts.Int)
-    new SeqTake(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(st: SeqTake) = Some((st.p0, st.p1))
+  override def actualCreate(args: (Term, Term)): SeqTake = new SeqTake(args._1, args._2)
 }
 
-class SeqLength(val p: Term) extends Term
-    with StructuralEqualityUnaryOp[Term] {
+class SeqLength private[terms] (val p: Term) extends Term
+    with ConditionalFlyweightUnaryOp[SeqLength] {
 
   val sort = sorts.Int
   override lazy val toString = s"|$p|"
 }
 
-object SeqLength {
-  def apply(t: Term) = {
+object SeqLength extends CondFlyweightTermFactory [Term, SeqLength] {
+  override def apply(t: Term) = {
     utils.assertSort(t, "term", "Seq", _.isInstanceOf[sorts.Seq])
-    new SeqLength(t)
+    createIfNonExistent(t)
   }
 
-  def unapply(sl: SeqLength) = Some(sl.p)
+  override def actualCreate(args: Term): SeqLength = new SeqLength(args)
 }
 
-class SeqAt(val p0: Term, val p1: Term) extends Term
-    with StructuralEqualityBinaryOp[Term] {
+class SeqAt private[terms] (val p0: Term, val p1: Term) extends Term
+    with ConditionalFlyweightBinaryOp[SeqAt] {
 
   val sort = p0.sort.asInstanceOf[sorts.Seq].elementsSort
 
   override lazy val toString = s"$p0[$p1]"
 }
 
-object SeqAt extends ((Term, Term) => Term) {
-  def apply(t0: Term, t1: Term) = {
+object SeqAt extends CondFlyweightTermFactory[(Term, Term), SeqAt] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq])
     utils.assertSort(t1, "second operand", sorts.Int)
-    new SeqAt(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(sa: SeqAt) = Some((sa.p0, sa.p1))
+  override def actualCreate(args: (Term, Term)): SeqAt = new SeqAt(args._1, args._2)
 }
 
-class SeqIn(val p0: Term, val p1: Term) extends BooleanTerm
-    with StructuralEqualityBinaryOp[Term] {
+class SeqIn private[terms] (val p0: Term, val p1: Term) extends BooleanTerm
+    with ConditionalFlyweightBinaryOp[SeqIn] {
 
   override lazy val toString = s"$p1 in $p0"
 }
 
-object SeqIn extends ((Term, Term) => BooleanTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SeqIn extends CondFlyweightTermFactory[(Term, Term), SeqIn] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq])
     utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Seq].elementsSort)
-    new SeqIn(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(si: SeqIn) = Some((si.p0, si.p1))
+  override def actualCreate(args: (Term, Term)): SeqIn = new SeqIn(args._1, args._2)
 }
 
-class SeqUpdate(val t0: Term, val t1: Term, val t2: Term)
+class SeqUpdate private[terms] (val t0: Term, val t1: Term, val t2: Term)
     extends SeqTerm
-       with StructuralEquality {
+       with ConditionalFlyweight[(Term, Term, Term), SeqUpdate] {
 
   val sort = t0.sort.asInstanceOf[sorts.Seq]
   val elementsSort = sort.elementsSort
-  val equalityDefiningMembers = t0 :: t1 :: t2 :: Nil
+  val equalityDefiningMembers = (t0, t1, t2)
   override lazy val toString = s"$t0[$t1] := $t2"
 }
 
-object SeqUpdate extends ((Term, Term, Term) => SeqTerm) {
-  def apply(t0: Term, t1: Term, t2: Term) = {
+object SeqUpdate extends CondFlyweightTermFactory[(Term, Term, Term), SeqUpdate] {
+  override def apply(v0: (Term, Term, Term)) = {
+    val (t0, t1, t2) = v0
     utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq])
     utils.assertSort(t1, "second operand", sorts.Int)
     utils.assertSort(t2, "third operand", t0.sort.asInstanceOf[sorts.Seq].elementsSort)
 
-    new SeqUpdate(t0, t1, t2)
+    createIfNonExistent(v0)
   }
 
-  def unapply(su: SeqUpdate) = Some((su.t0, su.t1, su.t2))
+  override def actualCreate(args: (Term, Term, Term)): SeqUpdate = new SeqUpdate(args._1, args._2, args._3)
 }
 
 /* Sets */
@@ -1480,27 +1676,37 @@ sealed trait SetTerm extends Term {
   val sort: sorts.Set
 }
 
-sealed trait BinarySetOp extends SetTerm
-    with StructuralEqualityBinaryOp[Term] {
-
+sealed trait BinarySetOp extends SetTerm {
+  val p0: Term
+  val p1: Term
   val elementsSort = p0.sort.asInstanceOf[sorts.Set].elementsSort
   val sort = sorts.Set(elementsSort)
 }
 
-case class EmptySet(elementsSort: Sort) extends SetTerm with Literal {
+class EmptySet private[terms] (val elementsSort: Sort) extends ConditionalFlyweight[Sort, EmptySet] with SetTerm with Literal {
   val sort = sorts.Set(elementsSort)
   override lazy val toString = "Ø"
+  override val equalityDefiningMembers: Sort = elementsSort
 }
 
-case class SingletonSet(p: Term) extends SetTerm /* with UnaryOp[Term] */ {
+object EmptySet extends CondFlyweightTermFactory[Sort, EmptySet] {
+  override def actualCreate(args: Sort): EmptySet = new EmptySet(args)
+}
+
+class SingletonSet private [terms] (val p: Term) extends ConditionalFlyweight[Term, SingletonSet] with SetTerm /* with UnaryOp[Term] */ {
   val elementsSort = p.sort
   val sort = sorts.Set(elementsSort)
 
   override lazy val toString = s"{$p}"
+  override val equalityDefiningMembers: Term = p
+}
+
+object SingletonSet extends PreciseCondFlyweightFactory[Term, SingletonSet] {
+  override def actualCreate(args: Term): SingletonSet = new SingletonSet(args)
 }
 
-class SetAdd(val p0: Term, val p1: Term) extends SetTerm
-    with StructuralEqualityBinaryOp[Term] {
+class SetAdd private[terms] (val p0: Term, val p1: Term) extends SetTerm
+    with ConditionalFlyweightBinaryOp[SetAdd] {
 
   val elementsSort = p0.sort.asInstanceOf[sorts.Set].elementsSort
   val sort = sorts.Set(elementsSort)
@@ -1508,115 +1714,122 @@ class SetAdd(val p0: Term, val p1: Term) extends SetTerm
   override val op = "+"
 }
 
-object SetAdd extends ((Term, Term) => SetTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SetAdd extends CondFlyweightTermFactory[(Term, Term), SetAdd] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSort(t0, "first operand", "Set", _.isInstanceOf[sorts.Set])
     utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Set].elementsSort)
 
-    new SetAdd(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(sa: SetAdd) = Some((sa.p0, sa.p1))
+  override def actualCreate(args: (Term, Term)): SetAdd = new SetAdd(args._1, args._2)
 }
 
-class SetUnion(val p0: Term, val p1: Term) extends BinarySetOp {
+class SetUnion(val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[SetUnion] with BinarySetOp {
   override val op = "∪"
 }
 
-object SetUnion extends ((Term, Term) => SetTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SetUnion extends PreciseCondFlyweightFactory[(Term, Term), SetUnion] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSameSorts[sorts.Set](t0, t1)
-    new SetUnion(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(su: SetUnion) = Some((su.p0, su.p1))
+  override def actualCreate(args: (Term, Term)): SetUnion = new SetUnion(args._1, args._2)
 }
 
-class SetIntersection(val p0: Term, val p1: Term) extends BinarySetOp {
+class SetIntersection private[terms] (val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[SetIntersection] with BinarySetOp {
   override val op = "∩"
 }
 
-object SetIntersection extends ((Term, Term) => SetTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SetIntersection extends PreciseCondFlyweightFactory[(Term, Term), SetIntersection] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSameSorts[sorts.Set](t0, t1)
-    new SetIntersection(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(si: SetIntersection) = Some((si.p0, si.p1))
+  override def actualCreate(args: (Term, Term)): SetIntersection = new SetIntersection(args._1, args._2)
 }
 
-class SetSubset(val p0: Term, val p1: Term) extends BooleanTerm 
-    with StructuralEqualityBinaryOp[Term] {
+class SetSubset private[terms] (val p0: Term, val p1: Term) extends BooleanTerm
+    with ConditionalFlyweightBinaryOp[SetSubset] {
   override val op = "⊂"
 }
 
-object SetSubset extends ((Term, Term) => BooleanTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SetSubset extends PreciseCondFlyweightFactory[(Term, Term), SetSubset] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSameSorts[sorts.Set](t0, t1)
-    new SetSubset(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(ss: SetSubset) = Some((ss.p0, ss.p1))
+  override def actualCreate(args: (Term, Term)): SetSubset = new SetSubset(args._1, args._2)
 }
 
-class SetDisjoint(val p0: Term, val p1: Term) extends BooleanTerm
-    with StructuralEqualityBinaryOp[Term] {
+class SetDisjoint private[terms] (val p0: Term, val p1: Term) extends BooleanTerm
+    with ConditionalFlyweightBinaryOp[SetDisjoint] {
   override val op = "disj"
 }
 
-object SetDisjoint extends ((Term, Term) => BooleanTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SetDisjoint extends PreciseCondFlyweightFactory[(Term, Term), SetDisjoint] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSameSorts[sorts.Set](t0, t1)
-    new SetDisjoint(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(sd: SetDisjoint) = Some((sd.p0, sd.p1))
+  override def actualCreate(args: (Term, Term)): SetDisjoint = new SetDisjoint(args._1, args._2)
 }
 
-class SetDifference(val p0: Term, val p1: Term) extends BinarySetOp {
+class SetDifference private[terms] (val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[SetDifference] with BinarySetOp {
   override val op = "\\"
 }
 
-object SetDifference extends ((Term, Term) => SetTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SetDifference extends PreciseCondFlyweightFactory[(Term, Term), SetDifference] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSameSorts[sorts.Set](t0, t1)
-    new SetDifference(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(sd: SetDifference) = Some((sd.p0, sd.p1))
+  override def actualCreate(args: (Term, Term)): SetDifference = new SetDifference(args._1, args._2)
 }
 
-class SetIn(val p0: Term, val p1: Term) extends BooleanTerm
-    with StructuralEqualityBinaryOp[Term] {
+class SetIn private[terms] (val p0: Term, val p1: Term) extends BooleanTerm
+    with ConditionalFlyweightBinaryOp[SetIn] {
 
   override val op = "in"
 }
 
-object SetIn extends ((Term, Term) => BooleanTerm) {
-  def apply(t0: Term, t1: Term) = {
+object SetIn extends PreciseCondFlyweightFactory[(Term, Term), SetIn] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSort(t1, "second operand", "Set", _.isInstanceOf[sorts.Set])
     utils.assertSort(t0, "first operand", t1.sort.asInstanceOf[sorts.Set].elementsSort)
 
-    new SetIn(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(si: SetIn) = Some((si.p0, si.p1))
+  override def actualCreate(args: (Term, Term)): SetIn = new SetIn(args._1, args._2)
 }
 
-class SetCardinality(val p: Term) extends Term
-    with StructuralEqualityUnaryOp[Term] {
+class SetCardinality private[terms] (val p: Term) extends Term
+    with ConditionalFlyweightUnaryOp[SetCardinality] {
 
   val sort = sorts.Int
   override lazy val toString = s"|$p|"
 }
 
-object SetCardinality extends (Term => SetCardinality) {
-  def apply(t: Term) = {
+object SetCardinality extends PreciseCondFlyweightFactory[Term, SetCardinality] {
+  override def apply(t: Term) = {
     utils.assertSort(t, "term", "Set", _.isInstanceOf[sorts.Set])
-    new SetCardinality(t)
+    createIfNonExistent(t)
   }
 
-  def unapply(sc: SetCardinality) = Some(sc.p)
+  override def actualCreate(args: Term): SetCardinality = new SetCardinality(args)
 }
 
 /* Multisets */
@@ -1626,130 +1839,143 @@ sealed trait MultisetTerm extends Term {
   val sort: sorts.Multiset
 }
 
-sealed trait BinaryMultisetOp extends MultisetTerm
-    with StructuralEqualityBinaryOp[Term] {
+sealed trait BinaryMultisetOp extends MultisetTerm {
 
+  val p0: Term
   val elementsSort = p0.sort.asInstanceOf[sorts.Multiset].elementsSort
   val sort = sorts.Multiset(elementsSort)
 }
 
-case class EmptyMultiset(elementsSort: Sort) extends MultisetTerm with Literal {
+class EmptyMultiset private[terms] (val elementsSort: Sort) extends MultisetTerm with Literal with ConditionalFlyweight[Sort, EmptyMultiset] {
   val sort = sorts.Multiset(elementsSort)
   override lazy val toString = "Ø"
+  override val equalityDefiningMembers: Sort = elementsSort
+}
+
+object EmptyMultiset extends PreciseCondFlyweightFactory[Sort, EmptyMultiset] {
+  override def actualCreate(args: Sort): EmptyMultiset = new EmptyMultiset(args)
 }
 
-case class SingletonMultiset(p: Term) extends MultisetTerm /* with UnaryOp[Term] */ {
+class SingletonMultiset private[terms] (val p: Term) extends MultisetTerm /* with UnaryOp[Term] */ with ConditionalFlyweight[Term, SingletonMultiset] {
   val elementsSort = p.sort
   val sort = sorts.Multiset(elementsSort)
 
   override lazy val toString = s"{$p}"
+  override val equalityDefiningMembers: Term = p
 }
 
-class MultisetAdd(val p0: Term, val p1: Term) extends MultisetTerm
-    with StructuralEqualityBinaryOp[Term] {
+object SingletonMultiset extends PreciseCondFlyweightFactory[Term, SingletonMultiset] {
+  override def actualCreate(args: Term): SingletonMultiset = new SingletonMultiset((args))
+}
 
-  val elementsSort = p0.sort.asInstanceOf[sorts.Multiset].elementsSort
-  val sort = sorts.Multiset(elementsSort)
+class MultisetAdd private[terms] (val p0: Term, val p1: Term) extends BinaryMultisetOp
+    with ConditionalFlyweightBinaryOp[MultisetAdd] {
 
   override val op = "+"
 }
 
-object MultisetAdd extends ((Term, Term) => MultisetTerm) {
-  def apply(t0: Term, t1: Term) = {
+object MultisetAdd extends PreciseCondFlyweightFactory[(Term, Term), MultisetAdd] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSort(t0, "first operand", "Set", _.isInstanceOf[sorts.Multiset])
     utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Multiset].elementsSort)
 
-    new MultisetAdd(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(ma: MultisetAdd) = Some((ma.p0, ma.p1))
+  override def actualCreate(args: (Term, Term)): MultisetAdd = new MultisetAdd(args._1, args._2)
 }
 
-class MultisetUnion(val p0: Term, val p1: Term) extends BinaryMultisetOp {
+class MultisetUnion private[terms] (val p0: Term, val p1: Term) extends BinaryMultisetOp with ConditionalFlyweightBinaryOp[MultisetUnion] {
   override val op = "∪"
 }
 
-object MultisetUnion extends ((Term, Term) => MultisetTerm) {
-  def apply(t0: Term, t1: Term) = {
+object MultisetUnion extends PreciseCondFlyweightFactory[(Term, Term), MultisetUnion] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSameSorts[sorts.Multiset](t0, t1)
-    new MultisetUnion(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(mu: MultisetUnion) = Some((mu.p0, mu.p1))
+  override def actualCreate(args: (Term, Term)): MultisetUnion = new MultisetUnion(args._1, args._2)
 }
 
-class MultisetIntersection(val p0: Term, val p1: Term) extends BinaryMultisetOp {
+class MultisetIntersection private[terms] (val p0: Term, val p1: Term) extends BinaryMultisetOp with ConditionalFlyweightBinaryOp[MultisetIntersection] {
   override val op = "∩"
 }
 
-object MultisetIntersection extends ((Term, Term) => MultisetTerm) {
-  def apply(t0: Term, t1: Term) = {
+object MultisetIntersection extends PreciseCondFlyweightFactory[(Term, Term), MultisetIntersection] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSameSorts[sorts.Multiset](t0, t1)
-    new MultisetIntersection(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(mi: MultisetIntersection) = Some((mi.p0, mi.p1))
+  override def actualCreate(args: (Term, Term)): MultisetIntersection = new MultisetIntersection(args._1, args._2)
 }
 
-class MultisetSubset(val p0: Term, val p1: Term) extends BooleanTerm
-    with StructuralEqualityBinaryOp[Term] {
+class MultisetSubset private[terms] (val p0: Term, val p1: Term) extends BooleanTerm
+    with ConditionalFlyweightBinaryOp[MultisetSubset] {
   override val op = "⊂"
 }
 
-object MultisetSubset extends ((Term, Term) => BooleanTerm) {
-  def apply(t0: Term, t1: Term) = {
+object MultisetSubset extends PreciseCondFlyweightFactory[(Term, Term), MultisetSubset] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSameSorts[sorts.Multiset](t0, t1)
-    new MultisetSubset(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(ms: MultisetSubset) = Some((ms.p0, ms.p1))
+  override def actualCreate(args: (Term, Term)): MultisetSubset = new MultisetSubset(args._1, args._2)
 }
 
-class MultisetDifference(val p0: Term, val p1: Term) extends BinaryMultisetOp {
+class MultisetDifference private[terms] (val p0: Term, val p1: Term) extends BinaryMultisetOp with ConditionalFlyweightBinaryOp[MultisetDifference] {
   override val op = "\\"
 }
 
-object MultisetDifference extends ((Term, Term) => MultisetTerm) {
-  def apply(t0: Term, t1: Term) = {
+object MultisetDifference extends PreciseCondFlyweightFactory[(Term, Term), MultisetDifference] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSameSorts[sorts.Multiset](t0, t1)
-    new MultisetDifference(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(md: MultisetDifference) = Some((md.p0, md.p1))
+  override def actualCreate(args: (Term, Term)): MultisetDifference = new MultisetDifference(args._1, args._2)
 }
 
-class MultisetCardinality(val p: Term) extends Term
-    with StructuralEqualityUnaryOp[Term] {
+class MultisetCardinality private[terms] (val p: Term) extends Term
+    with ConditionalFlyweightUnaryOp[MultisetCardinality] {
 
   val sort = sorts.Int
   override lazy val toString = s"|$p|"
 }
 
-object MultisetCardinality extends (Term => MultisetCardinality) {
-  def apply(t: Term) = {
+object MultisetCardinality extends PreciseCondFlyweightFactory[Term, MultisetCardinality] {
+  override def apply(t: Term) = {
     utils.assertSort(t, "term", "Multiset", _.isInstanceOf[sorts.Multiset])
-    new MultisetCardinality(t)
+    createIfNonExistent(t)
   }
 
-  def unapply(mc: MultisetCardinality) = Some(mc.p)
+  override def actualCreate(args: Term): MultisetCardinality = new MultisetCardinality(args)
 }
 
-class MultisetCount(val p0: Term, val p1: Term) extends Term
-    with StructuralEqualityBinaryOp[Term] {
+class MultisetCount private[terms] (val p0: Term, val p1: Term) extends Term
+    with ConditionalFlyweightBinaryOp[MultisetCount] {
 
   val sort = sorts.Int
   override lazy val toString = s"$p0($p1)"
 }
 
-object MultisetCount extends {
-  def apply(ms: Term, el: Term) = {
+object MultisetCount extends PreciseCondFlyweightFactory[(Term, Term), MultisetCount] {
+  override def apply(v0: (Term, Term)) = {
+    val (ms, el) = v0
     utils.assertSort(ms, "first operand", "Multiset", _.isInstanceOf[sorts.Multiset])
     utils.assertSort(el, "second operand", ms.sort.asInstanceOf[sorts.Multiset].elementsSort)
 
-    new MultisetCount(ms, el)
+    createIfNonExistent(v0)
   }
 
-  def unapply(mc: MultisetCount) = Some((mc.p0, mc.p1))
+  override def actualCreate(args: (Term, Term)): MultisetCount = new MultisetCount(args._1, args._2)
 }
 
 /* Maps */
@@ -1760,88 +1986,95 @@ sealed trait MapTerm extends Term {
   val sort: sorts.Map
 }
 
-case class EmptyMap(keySort: Sort, valueSort: Sort) extends MapTerm with Literal {
+class EmptyMap private[terms] (val keySort: Sort, val valueSort: Sort) extends MapTerm with Literal with ConditionalFlyweight[(Sort, Sort), EmptyMap] {
   val sort = sorts.Map(keySort, valueSort)
   override lazy val toString = "Ø"
+  override val equalityDefiningMembers: (Sort, Sort) = (keySort, valueSort)
+}
+
+object EmptyMap extends PreciseCondFlyweightFactory[(Sort, Sort), EmptyMap] {
+  override def actualCreate(args: (Sort, Sort)): EmptyMap = new EmptyMap(args._1, args._2)
 }
 
-class MapLookup(base: Term, key: Term) extends Term with StructuralEqualityBinaryOp[Term] {
+class MapLookup private[terms] (val base: Term, val key: Term) extends Term with ConditionalFlyweightBinaryOp[MapLookup] {
   val sort: Sort = p0.sort.asInstanceOf[sorts.Map].valueSort
   override def p0: Term = base
   override def p1: Term = key
   override lazy val toString = s"$p0[$p1]"
 }
 
-object MapLookup extends ((Term, Term) => Term) {
-  def apply(t0: Term, t1: Term) : Term = {
+object MapLookup extends PreciseCondFlyweightFactory[(Term, Term), MapLookup] {
+  override def apply(v0: (Term, Term)) = {
+    val (t0, t1) = v0
     utils.assertSort(t0, "first operand", "Map", _.isInstanceOf[sorts.Map])
     utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Map].keySort)
-    new MapLookup(t0, t1)
+    createIfNonExistent(v0)
   }
 
-  def unapply(ml: MapLookup) = Some((ml.p0, ml.p1))
+  override def actualCreate(args: (Term, Term)): MapLookup = new MapLookup(args._1, args._2)
 }
 
-class MapCardinality(val p: Term) extends Term with StructuralEqualityUnaryOp[Term] {
+class MapCardinality private[terms] (val p: Term) extends Term with ConditionalFlyweightUnaryOp[MapCardinality] {
   val sort = sorts.Int
   override lazy val toString = s"|$p|"
 }
 
-object MapCardinality extends (Term => MapCardinality) {
-  def apply(t: Term) : MapCardinality = {
+object MapCardinality extends PreciseCondFlyweightFactory[Term, MapCardinality] {
+  override def apply(t: Term) : MapCardinality = {
     utils.assertSort(t, "term", "Map", _.isInstanceOf[sorts.Map])
-    new MapCardinality(t)
+    createIfNonExistent(t)
   }
 
-  def unapply(mc: MapCardinality) = Some(mc.p)
+  override def actualCreate(args: Term): MapCardinality = new MapCardinality(args)
 }
 
-class MapUpdate(val base: Term, val key: Term, val value: Term) extends MapTerm with StructuralEquality {
+class MapUpdate private[terms] (val base: Term, val key: Term, val value: Term) extends MapTerm with ConditionalFlyweight[(Term, Term, Term), MapUpdate] {
   override val sort: sorts.Map = base.sort.asInstanceOf[sorts.Map]
   override val keySort: Sort = sort.keySort
   override val valueSort: Sort = sort.valueSort
-  override val equalityDefiningMembers: Seq[Any] = Seq(base, key, value)
+  override val equalityDefiningMembers = (base, key, value)
 }
 
-object MapUpdate extends ((Term, Term, Term) => MapTerm) {
-  def apply(t0: Term, t1: Term, t2: Term) : MapUpdate = {
+object MapUpdate extends PreciseCondFlyweightFactory[(Term, Term, Term), MapUpdate] {
+  override def apply(v0: (Term, Term, Term)) : MapUpdate = {
+    val (t0, t1, t2) = v0
     utils.assertSort(t0, "first operand", "Map", _.isInstanceOf[sorts.Map])
     utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Map].keySort)
     utils.assertSort(t2, "third operand", t0.sort.asInstanceOf[sorts.Map].valueSort)
-    new MapUpdate(t0, t1, t2)
+    createIfNonExistent(v0)
   }
 
-  def unapply(mu: MapUpdate) = Some((mu.base, mu.key, mu.value))
+  override def actualCreate(args: (Term, Term, Term)): MapUpdate = new MapUpdate(args._1, args._2, args._3)
 }
 
-class MapDomain(val p: Term) extends SetTerm with StructuralEqualityUnaryOp[Term] {
+class MapDomain private[terms] (val p: Term) extends SetTerm with ConditionalFlyweightUnaryOp[MapDomain] {
   override val elementsSort: Sort = p.sort.asInstanceOf[sorts.Map].keySort
   override val sort: sorts.Set = sorts.Set(elementsSort)
   override lazy val toString = s"domain($p)"
 }
 
-object MapDomain extends (Term => SetTerm) {
-  def apply(t0: Term) : SetTerm = {
+object MapDomain extends PreciseCondFlyweightFactory[Term, MapDomain] {
+  override def apply(t0: Term) = {
     utils.assertSort(t0, "term", "Map", _.isInstanceOf[sorts.Map])
-    new MapDomain(t0)
+    createIfNonExistent(t0)
   }
 
-  def unapply(md : MapDomain) = Some(md.p)
+  override def actualCreate(args: Term): MapDomain = new MapDomain(args)
 }
 
-class MapRange(val p: Term) extends SetTerm with StructuralEqualityUnaryOp[Term] {
+class MapRange private[terms] (val p: Term) extends SetTerm with ConditionalFlyweightUnaryOp[MapRange] {
   override val elementsSort: Sort = p.sort.asInstanceOf[sorts.Map].valueSort
   override val sort: sorts.Set = sorts.Set(elementsSort)
   override lazy val toString = s"range($p)"
 }
 
-object MapRange extends (Term => SetTerm) {
-  def apply(t0: Term) : SetTerm = {
+object MapRange extends PreciseCondFlyweightFactory[Term, MapRange] {
+  override def apply(t0: Term) = {
     utils.assertSort(t0, "term", "Map", _.isInstanceOf[sorts.Map])
-    new MapRange(t0)
+    createIfNonExistent(t0)
   }
 
-  def unapply(mr : MapRange) = Some(mr.p)
+  override def actualCreate(args: Term): MapRange = new MapRange(args)
 }
 
 /* Snapshots */
@@ -1849,7 +2082,7 @@ object MapRange extends (Term => SetTerm) {
 sealed trait SnapshotTerm extends Term { val sort = sorts.Snap }
 
 class Combine(val p0: Term, val p1: Term) extends SnapshotTerm
-    with StructuralEqualityBinaryOp[Term] {
+    with ConditionalFlyweightBinaryOp[Combine] {
 
   utils.assertSort(p0, "first operand", sorts.Snap)
   utils.assertSort(p1, "second operand", sorts.Snap)
@@ -1857,103 +2090,143 @@ class Combine(val p0: Term, val p1: Term) extends SnapshotTerm
   override lazy val toString = s"($p0, $p1)"
 }
 
-object Combine extends ((Term, Term) => Term) {
-  def apply(t0: Term, t1: Term) = new Combine(t0.convert(sorts.Snap), t1.convert(sorts.Snap))
+object Combine extends CondFlyweightTermFactory[(Term, Term), Combine] {
+  override def apply(v0: (Term, Term)) = createIfNonExistent(v0._1.convert(sorts.Snap), v0._2.convert(sorts.Snap))
 
-  def unapply(c: Combine) = Some((c.p0, c.p1))
+  override def actualCreate(args: (Term, Term)): Combine = new Combine(args._1, args._2)
 }
 
 class First(val p: Term) extends SnapshotTerm
-    with StructuralEqualityUnaryOp[Term]
+    with ConditionalFlyweightUnaryOp[First]
     /*with PossibleTrigger*/ {
 
   utils.assertSort(p, "term", sorts.Snap)
 }
 
-object First extends (Term => Term) {
-  def apply(t: Term) = t match {
+object First extends CondFlyweightTermFactory[Term, First] {
+  override def apply(t: Term) = t match {
     case Combine(t1, _) => t1
-    case _ => new First(t)
+    case _ => createIfNonExistent(t)
   }
 
-  def unapply(f: First) = Some(f.p)
+  override def actualCreate(args: Term): First = new First(args)
 }
 
 class Second(val p: Term) extends SnapshotTerm
-    with StructuralEqualityUnaryOp[Term]
+    with ConditionalFlyweightUnaryOp[Second]
     /*with PossibleTrigger*/ {
 
   utils.assertSort(p, "term", sorts.Snap)
 }
 
-object Second extends (Term => Term) {
-  def apply(t: Term) = t match {
+object Second extends CondFlyweightTermFactory[Term, Second] {
+  override def apply(t: Term) = t match {
     case Combine(_, t2) => t2
-    case _ => new Second(t)
+    case _ => createIfNonExistent(t)
   }
 
-  def unapply(s: Second) = Some(s.p)
+  override def actualCreate(args: Term): Second = new Second(args)
 }
 
 /* Quantified permissions */
 
-case class Lookup(field: String, fvf: Term, at: Term) extends Term {
+class Lookup(val field: String, val fvf: Term, val at: Term) extends Term with ConditionalFlyweight[(String, Term, Term), Lookup] {
   utils.assertSort(fvf, "field value function", "FieldValueFunction", _.isInstanceOf[sorts.FieldValueFunction])
   utils.assertSort(at, "receiver", sorts.Ref)
 
+  override val equalityDefiningMembers: (String, Term, Term) = (field, fvf, at)
   val sort = fvf.sort.asInstanceOf[sorts.FieldValueFunction].codomainSort
 }
 
-case class PermLookup(field: String, pm: Term, at: Term) extends Term {
+object Lookup extends PreciseCondFlyweightFactory[(String, Term, Term), Lookup] {
+  override def actualCreate(args: (String, Term, Term)): Lookup = new Lookup(args._1, args._2, args._3)
+}
+
+class PermLookup(val field: String, val pm: Term, val at: Term) extends Term with ConditionalFlyweight[(String, Term, Term), PermLookup] {
   utils.assertSort(pm, "field perm function", "FieldPermFunction", _.isInstanceOf[sorts.FieldPermFunction])
   utils.assertSort(at, "receiver", sorts.Ref)
 
+  override val equalityDefiningMembers: (String, Term, Term) = (field, pm, at)
   val sort = sorts.Perm
 }
 
-case class Domain(field: String, fvf: Term) extends SetTerm /*with PossibleTrigger*/ {
+object PermLookup extends PreciseCondFlyweightFactory[(String, Term, Term), PermLookup] {
+  override def actualCreate(args: (String, Term, Term)): PermLookup = new PermLookup(args._1, args._2, args._3)
+}
+
+class Domain(val field: String, val fvf: Term) extends SetTerm /*with PossibleTrigger*/ with ConditionalFlyweight[(String, Term), Domain] {
   utils.assertSort(fvf, "field value function", "FieldValueFunction", _.isInstanceOf[sorts.FieldValueFunction])
 
   val elementsSort = sorts.Ref
   val sort = sorts.Set(elementsSort)
+  override val equalityDefiningMembers: (String, Term) = (field, fvf)
 }
 
-case class FieldTrigger(field: String, fvf: Term, at: Term) extends Term {
+object Domain extends CondFlyweightTermFactory[(String, Term), Domain] {
+  override def actualCreate(args: (String, Term)): Domain = new Domain(args._1, args._2)
+}
+
+class FieldTrigger(val field: String, val fvf: Term, val at: Term) extends Term with ConditionalFlyweight[(String, Term, Term), FieldTrigger] {
   utils.assertSort(fvf, "field value function", "FieldValueFunction", _.isInstanceOf[sorts.FieldValueFunction])
   utils.assertSort(at, "receiver", sorts.Ref)
 
   val sort = sorts.Bool
+  override val equalityDefiningMembers: (String, Term, Term) = (field, fvf, at)
+}
+
+object FieldTrigger extends PreciseCondFlyweightFactory[(String, Term, Term), FieldTrigger] {
+  override def actualCreate(args: (String, Term, Term)): FieldTrigger = new FieldTrigger(args._1, args._2, args._3)
 }
 
 /* Quantified predicates */
 
-case class PredicateLookup(predname: String, psf: Term, args: Seq[Term]) extends Term {
+class PredicateLookup(val predname: String, val psf: Term, val args: Seq[Term]) extends Term with ConditionalFlyweight[(String, Term, Seq[Term]), PredicateLookup] {
   utils.assertSort(psf, "predicate snap function", "PredicateSnapFunction", _.isInstanceOf[sorts.PredicateSnapFunction])
 
   val sort = psf.sort.asInstanceOf[sorts.PredicateSnapFunction].codomainSort
+  override val equalityDefiningMembers: (String, Term, Seq[Term]) = (predname, psf, args)
 }
 
-case class PredicatePermLookup(predname: String, pm: Term, args: Seq[Term]) extends Term {
+object PredicateLookup extends PreciseCondFlyweightFactory[(String, Term, Seq[Term]), PredicateLookup] {
+  override def actualCreate(args: (String, Term, Seq[Term])): PredicateLookup = new PredicateLookup(args._1, args._2, args._3)
+}
+
+class PredicatePermLookup(val predname: String, val pm: Term, val args: Seq[Term]) extends Term with ConditionalFlyweight[(String, Term, Seq[Term]), PredicatePermLookup] {
   utils.assertSort(pm, "predicate perm function", "PredicatePermFunction", _.isInstanceOf[sorts.PredicatePermFunction])
 
   val sort = sorts.Perm
+  override val equalityDefiningMembers: (String, Term, Seq[Term]) = (predname, pm, args)
 }
 
-case class PredicateDomain(predname: String, psf: Term) extends SetTerm /*with PossibleTrigger*/ {
+object PredicatePermLookup extends PreciseCondFlyweightFactory[(String, Term, Seq[Term]), PredicatePermLookup] {
+  override def actualCreate(args: (String, Term, Seq[Term])): PredicatePermLookup = new PredicatePermLookup(args._1, args._2, args._3)
+}
+
+class PredicateDomain(val predname: String, val psf: Term) extends SetTerm /*with PossibleTrigger*/ with ConditionalFlyweight[(String, Term), PredicateDomain] {
   utils.assertSort(psf, "predicate snap function", "PredicateSnapFunction", _.isInstanceOf[sorts.PredicateSnapFunction])
   val elementsSort = sorts.Snap
   val sort = sorts.Set(elementsSort)
+  override val equalityDefiningMembers: (String, Term) = (predname, psf)
 }
 
-case class PredicateTrigger(predname: String, psf: Term, args: Seq[Term]) extends Term {
+object PredicateDomain extends CondFlyweightTermFactory[(String, Term), PredicateDomain] {
+  override def actualCreate(args: (String, Term)): PredicateDomain = new PredicateDomain(args._1, args._2)
+}
+
+class PredicateTrigger(val predname: String, val psf: Term, val args: Seq[Term]) extends Term with ConditionalFlyweight[(String, Term, Seq[Term]), PredicateTrigger] {
   utils.assertSort(psf, "predicate snap function", "PredicateSnapFunction", _.isInstanceOf[sorts.PredicateSnapFunction])
 
   val sort = sorts.Bool
+  override val equalityDefiningMembers: (String, Term, Stack[Term]) = (predname, psf, args)
+}
+
+object PredicateTrigger extends PreciseCondFlyweightFactory[(String, Term, Seq[Term]), PredicateTrigger] {
+  override def actualCreate(args: (String, Term, Seq[Term])): PredicateTrigger = new PredicateTrigger(args._1, args._2, args._3)
 }
 
 /* Magic wands */
 
-case class MagicWandSnapshot(abstractLhs: Term, rhsSnapshot: Term) extends Combine(abstractLhs, rhsSnapshot) {
+class MagicWandSnapshot(val abstractLhs: Term, val rhsSnapshot: Term) extends Combine(abstractLhs, rhsSnapshot) {
   utils.assertSort(abstractLhs, "abstract lhs", sorts.Snap)
   utils.assertSort(rhsSnapshot, "rhs", sorts.Snap)
 
@@ -1969,7 +2242,7 @@ case class MagicWandSnapshot(abstractLhs: Term, rhsSnapshot: Term) extends Combi
   }
 }
 
-object MagicWandSnapshot {
+object MagicWandSnapshot  {
   def apply(snapshot: Term): MagicWandSnapshot = {
     assert(snapshot.sort == sorts.Snap)
     snapshot match {
@@ -1978,20 +2251,43 @@ object MagicWandSnapshot {
         MagicWandSnapshot(First(snapshot), Second(snapshot))
     }
   }
+
+  // Since MagicWandSnapshot subclasses Combine, we apparently cannot inherit the normal subclass, so we
+  // have to copy paste the code here.
+  var pool = new TrieMap[(Term, Term), MagicWandSnapshot]()
+
+  def createIfNonExistent(args: (Term, Term)): MagicWandSnapshot = {
+    if (Verifier.config.useFlyweight) {
+      pool.getOrElseUpdate(args, actualCreate(args))
+    } else {
+      actualCreate(args)
+    }
+  }
+
+  def actualCreate(tuple: (Term, Term)) = new MagicWandSnapshot(tuple._1, tuple._2)
+  def apply(fst: Term, snd: Term): MagicWandSnapshot = createIfNonExistent((fst, snd))
+
+  def unapply(mws: MagicWandSnapshot) = Some((mws.abstractLhs, mws.rhsSnapshot))
 }
 
-case class MagicWandChunkTerm(chunk: MagicWandChunk) extends Term {
+class MagicWandChunkTerm(val chunk: MagicWandChunk) extends Term with ConditionalFlyweight[MagicWandChunk, MagicWandChunkTerm] {
   override val sort = sorts.Unit /* TODO: Does this make sense? */
   override lazy val toString = s"wand@${chunk.id.ghostFreeWand.pos}}"
+  override val equalityDefiningMembers: MagicWandChunk = chunk
+}
+
+object MagicWandChunkTerm extends CondFlyweightTermFactory[MagicWandChunk, MagicWandChunkTerm] {
+  override def actualCreate(args: MagicWandChunk): MagicWandChunkTerm = new MagicWandChunkTerm(args)
 }
 
 /* Factory methods for all resources */
 
 object toSnapTree extends (Seq[Term] => Term) {
+  private def binaryCombine(t0: Term, t1: Term) = Combine(t0, t1)
   @inline
   def apply(args: Seq[Term]): Term = {
     if (args.isEmpty) Unit
-    else args.map(_.convert(sorts.Snap)).reduceLeft(Combine)
+    else args.map(_.convert(sorts.Snap)).reduceLeft(binaryCombine)
   }
 }
 
@@ -2100,63 +2396,64 @@ object PsfTop extends (String => Identifier) {
  */
 class SortWrapper(val t: Term, val to: Sort)
     extends Term
-       with StructuralEquality {
+       with ConditionalFlyweight[(Term, Sort), SortWrapper] {
 
   assert((t.sort == sorts.Snap || to == sorts.Snap) && t.sort != to,
          s"Unexpected sort wrapping of $t from ${t.sort} to $to")
 
-  val equalityDefiningMembers = t :: to :: Nil
+  val equalityDefiningMembers = (t, to)
 //  override lazy val toString = s"SortWrapper($t, $to)"
   override lazy val toString = t.toString
   override val sort = to
 }
 
-object SortWrapper {
-  def apply(t: Term, to: Sort) = t match {
-    case _ if t.sort == to => t
-    case sw: SortWrapper if sw.t.sort == to => sw.t
-    case _ => new SortWrapper(t, to)
+object SortWrapper extends CondFlyweightTermFactory[(Term, Sort), SortWrapper] {
+  override def apply(v0: (Term, Sort)) = v0 match {
+    case (t, to) if t.sort == to => t
+    case (sw: SortWrapper, to) if sw.t.sort == to => sw.t
+    case _ => createIfNonExistent(v0)
   }
 
-  def unapply(sw: SortWrapper) = Some((sw.t, sw.to))
+  override def actualCreate(args: (Term, Sort)): SortWrapper = new SortWrapper(args._1, args._2)
 }
 
 /* Other terms */
 
-class Distinct(val ts: Set[DomainFun]) extends BooleanTerm with StructuralEquality {
+class Distinct(val ts: Set[DomainFun]) extends BooleanTerm with ConditionalFlyweight[Set[DomainFun], Distinct] {
   assert(ts.size >= 2, "Distinct requires at least two terms")
 
-  val equalityDefiningMembers = ts :: Nil
+  val equalityDefiningMembers = ts
   override lazy val toString = s"Distinct($ts)"
 }
 
-object Distinct extends (Set[DomainFun] => Term) {
-  def apply(ts: Set[DomainFun]): Term =
-    if (ts.size >= 2) new Distinct(ts)
-    else True()
+object Distinct extends CondFlyweightTermFactory[Set[DomainFun], Distinct] {
+  override def apply(ts: Set[DomainFun]): Term =
+    if (ts.size >= 2) createIfNonExistent(ts)
+    else True
 
-  def unapply(d: Distinct) = Some(d.ts)
+  override def actualCreate(args: Set[DomainFun]): Distinct = new Distinct(args)
 }
 
-class Let(val bindings: Map[Var, Term], val body: Term) extends Term with StructuralEquality {
+class Let(val bindings: Map[Var, Term], val body: Term) extends Term with ConditionalFlyweight[(Map[Var, Term], Term), Let] {
   assert(bindings.nonEmpty, "Let needs to bind at least one variable")
 
   val sort = body.sort
-  val equalityDefiningMembers = Seq(body) ++ bindings.flatMap(_.productIterator)
+  val equalityDefiningMembers = (bindings, body)
 
   override lazy val toString = s"let ${bindings.map(p => s"${p._1} = ${p._2}")} in $body"
 }
 
-object Let extends ((Map[Var, Term], Term) => Term) {
+object Let extends CondFlyweightTermFactory[(Map[Var, Term], Term), Let] {
   def apply(v: Var, t: Term, body: Term): Term = apply(Map(v -> t), body)
   def apply(vs: Seq[Var], ts: Seq[Term], body: Term): Term = apply(toMap(vs zip ts), body)
 
-  def apply(bindings: Map[Var, Term], body: Term) = {
+  override def apply(v0: (Map[Var, Term], Term)) = {
+    val (bindings, body) = v0
     if (bindings.isEmpty) body
-    else new Let(bindings, body)
+    else createIfNonExistent(v0)
   }
 
-  def unapply(l: Let) = Some((l.bindings, l.body))
+  override def actualCreate(args: (Map[Var, Term], Term)): Let = new Let(args._1, args._2)
 }
 
 /* Predefined terms */
@@ -2173,23 +2470,25 @@ object predef {
 
 object perms {
   def IsNonNegative(p: Term): Term =
-    Or(p === NoPerm(), IsPositive(p))
+    Or(p === NoPerm, IsPositive(p))
       /* All basic static simplifications should be covered by Equals,
        * IsPositive and or
        */
 
   def IsPositive(p: Term): Term = p match {
-    case p: PermLiteral => if (p.literal > Rational.zero) True() else False()
-    case _ => PermLess(NoPerm(), p)
+    case p: PermLiteral => if (p.literal > Rational.zero) True else False
+    case _ => PermLess(NoPerm, p)
   }
 
   def IsNonPositive(p: Term): Term = p match {
-    case p: PermLiteral => if (p.literal <= Rational.zero) True() else False()
-    case _ => Or(p === NoPerm(), PermLess(p, NoPerm()))
+    case p: PermLiteral => if (p.literal <= Rational.zero) True else False
+    case _ => Or(p === NoPerm, PermLess(p, NoPerm))
   }
 
-  def BigPermSum(it: Iterable[Term], f: Term => Term = t => t): Term =
-    viper.silicon.utils.mapReduceLeft(it, f, PermPlus, NoPerm())
+  def BigPermSum(it: Iterable[Term], f: Term => Term = t => t): Term = {
+    def binaryPermPlus(t0: Term, t1: Term) = PermPlus(t0, t1)
+    viper.silicon.utils.mapReduceLeft(it, f, binaryPermPlus, NoPerm)
+  }
 }
 
 /* Utility functions */
@@ -2261,5 +2560,5 @@ object implicits {
   import scala.language.implicitConversions
 
   implicit def intToTerm(i: Int): IntLiteral = IntLiteral(i)
-  implicit def boolToTerm(b: Boolean): BooleanLiteral = if (b) True() else False()
+  implicit def boolToTerm(b: Boolean): BooleanLiteral = if (b) True else False
 }
diff --git a/src/main/scala/state/Triggers.scala b/src/main/scala/state/Triggers.scala
index 757e25440..b03048530 100644
--- a/src/main/scala/state/Triggers.scala
+++ b/src/main/scala/state/Triggers.scala
@@ -80,7 +80,7 @@ class TriggerGenerator
   }
 
   /* True iff the given node is a possible trigger */
-  def isPossibleTrigger(e: Term): Boolean = e match {
+  def isPossibleTrigger(e: Term): Boolean = (customIsPossibleTrigger orElse {
     case _: Var => false
     case app: App => app.applicable.isInstanceOf[Function]
     case   _: CustomEquals
@@ -106,11 +106,10 @@ class TriggerGenerator
          | _: PredicateLookup
          => true
     case _ => false
-  }
+  }: PartialFunction[Term, Boolean])(e)
 
   /* True iff the given node is not allowed in triggers */
-  def isForbiddenInTrigger(term: Term) = term match {
-    case app: App => app.applicable.isInstanceOf[Macro]
+  def isForbiddenInTrigger(term: Term) = (customIsForbiddenInTrigger orElse {
     case   _: Plus | _: Minus | _: Times | _: Div | _: Mod
          | _: Not | _: Or | _: And | _: Implies | _: Iff | _: Ite
          | _: BuiltinEquals
@@ -118,10 +117,9 @@ class TriggerGenerator
          | _: PermTimes | _: IntPermTimes | _: PermIntDiv | _: PermPermDiv |_: PermPlus | _: PermMinus
          | _: PermLess | _: PermAtMost
          | _: Distinct
-         | _: Let
          => true
     case _ => false
-  }
+  }: PartialFunction[Term, Boolean])(term)
 
   val advancedIsForbiddenInTrigger:PartialFunction[Term, Boolean] = {
     case _: Plus | _: Minus => false
diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala
index 10bf5c580..353dac8c1 100644
--- a/src/main/scala/supporters/ExpressionTranslator.scala
+++ b/src/main/scala/supporters/ExpressionTranslator.scala
@@ -40,9 +40,18 @@ trait ExpressionTranslator {
       }
 
     def translateAnySetBinExp(exp: ast.AnySetBinExp,
+                              setTerm: ((Term, Term)) => Term,
+                              multisetTerm: ((Term, Term)) => Term,
+                              anysetTypedExp: ast.Exp = exp): Term = {
+      def setFun(t0: Term, t1: Term): Term = setTerm((t0, t1))
+      def multisetFun(t0: Term, t1: Term): Term = multisetTerm((t0, t1))
+      actualTranslateAnySetBinExp(exp, setFun _, multisetFun _, anysetTypedExp)
+    }
+
+    def actualTranslateAnySetBinExp(exp: ast.AnySetBinExp,
                               setTerm: (Term, Term) => Term,
                               multisetTerm: (Term, Term) => Term,
-                              anysetTypedExp: ast.Exp = exp) =
+                              anysetTypedExp: ast.Exp = exp): Term =
 
       anysetTypedExp.typ match {
         case _: ast.SetType => setTerm(f(exp.left), f(exp.right))
@@ -102,8 +111,8 @@ trait ExpressionTranslator {
                        false,
                        weight)
 
-      case _: ast.TrueLit => True()
-      case _: ast.FalseLit => False()
+      case _: ast.TrueLit => True
+      case _: ast.FalseLit => False
       case ast.Not(e0) => Not(f(e0))
       case ast.And(e0, e1) => And(f(e0), f(e1))
       case ast.Or(e0, e1) => Or(f(e0), f(e1))
@@ -126,7 +135,7 @@ trait ExpressionTranslator {
       case ast.LeCmp(e0, e1) => AtMost(f(e0), f(e1))
       case ast.LtCmp(e0, e1) => Less(f(e0), f(e1))
 
-      case _: ast.NullLit => Null()
+      case _: ast.NullLit => Null
 
       case v: ast.AbstractLocalVar => Var(Identifier(v.name), toSort(v.typ))
 
@@ -148,11 +157,11 @@ trait ExpressionTranslator {
 
       /* Permissions */
 
-      case _: ast.FullPerm => FullPerm()
-      case _: ast.NoPerm => NoPerm()
+      case _: ast.FullPerm => FullPerm
+      case _: ast.NoPerm => NoPerm
       case ast.FractionalPerm(e0, e1) => FractionPerm(f(e0), f(e1))
 
-      case ast.PermMinus(e0) => PermMinus(NoPerm(), f(e0))
+      case ast.PermMinus(e0) => PermMinus(NoPerm, f(e0))
       case ast.PermAdd(e0, e1) => PermPlus(f(e0), f(e1))
       case ast.PermSub(e0, e1) => PermMinus(f(e0), f(e1))
       case ast.PermMul(e0, e1) => PermTimes(f(e0), f(e1))
@@ -197,7 +206,7 @@ trait ExpressionTranslator {
       case as: ast.AnySetIntersection => translateAnySetBinExp(as, SetIntersection, MultisetIntersection)
       case as: ast.AnySetSubset => translateAnySetBinExp(as, SetSubset, MultisetSubset, as.left)
       case as: ast.AnySetMinus => translateAnySetBinExp(as, SetDifference, MultisetDifference)
-      case as: ast.AnySetContains => translateAnySetBinExp(as, SetIn, (t0, t1) => MultisetCount(t1, t0), as.right)
+      case as: ast.AnySetContains => translateAnySetBinExp(as, SetIn, { case (t0, t1) => MultisetCount(t1, t0) }, as.right)
       case as: ast.AnySetCardinality => translateAnySetUnExp(as, SetCardinality, MultisetCardinality, as.exp)
 
       /* Maps */
diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
index c1cdbce9d..81aa923a1 100644
--- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
+++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
@@ -87,8 +87,8 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
                                   : Term =
 
     e match {
-      case _: ast.AccessPredicate | _: ast.MagicWand if ignoreAccessPredicates => True()
-      case q: ast.Forall if !q.isPure && ignoreAccessPredicates => True()
+      case _: ast.AccessPredicate | _: ast.MagicWand if ignoreAccessPredicates => True
+      case q: ast.Forall if !q.isPure && ignoreAccessPredicates => True
 
       case _: ast.Result => data.formalResult
 
diff --git a/src/test/scala/SimpleArithmeticTermSolverTests.scala b/src/test/scala/SimpleArithmeticTermSolverTests.scala
index eee936d23..77e623906 100644
--- a/src/test/scala/SimpleArithmeticTermSolverTests.scala
+++ b/src/test/scala/SimpleArithmeticTermSolverTests.scala
@@ -9,12 +9,19 @@ package viper.silicon.tests
 import org.scalatest.matchers.should.Matchers
 import viper.silicon.state.Identifier
 import DSL._
+import org.scalatest.BeforeAndAfter
 import org.scalatest.funsuite.AnyFunSuite
+import viper.silicon.Config
 import viper.silicon.state.terms._
+import viper.silicon.verifier.Verifier
 
-class SimpleArithmeticTermSolverTests extends AnyFunSuite with Matchers {
+class SimpleArithmeticTermSolverTests extends AnyFunSuite with Matchers with BeforeAndAfter {
   import SimpleArithmeticSolver.{solve, SolverResult, SolvingSuccess, SolvingFailure}
 
+  before {
+    Verifier.config = new Config(Seq())
+  }
+
   test("Pre-solving errors") {
     assert(solve(b, y, y).isInstanceOf[SolverResult])
     assert(solve(x, b, y).isInstanceOf[SolverResult])
diff --git a/src/test/scala/TriggerGeneratorTests.scala b/src/test/scala/TriggerGeneratorTests.scala
index afe163500..2a7b831b9 100644
--- a/src/test/scala/TriggerGeneratorTests.scala
+++ b/src/test/scala/TriggerGeneratorTests.scala
@@ -6,13 +6,20 @@
 
 package viper.silicon.tests
 
+import org.scalatest.BeforeAndAfter
 import org.scalatest.funsuite.AnyFunSuite
+import viper.silicon.Config
 import viper.silicon.state.Identifier
 import viper.silicon.state.terms._
+import viper.silicon.verifier.Verifier
 
-class TriggerGeneratorTests extends AnyFunSuite {
+class TriggerGeneratorTests extends AnyFunSuite with BeforeAndAfter {
   val triggerGenerator = new TriggerGenerator()
 
+  before {
+    Verifier.config = new Config(Seq())
+  }
+
   test("Work in simple cases") {
     val i = Var(Identifier("i"), sorts.Int)
     val s = Var(Identifier("S"), sorts.Seq(sorts.Int))
diff --git a/src/test/scala/TriggerRewriterTests.scala b/src/test/scala/TriggerRewriterTests.scala
index 7f5df140b..e9ad7c5fe 100644
--- a/src/test/scala/TriggerRewriterTests.scala
+++ b/src/test/scala/TriggerRewriterTests.scala
@@ -7,14 +7,16 @@
 package viper.silicon.tests
 
 import java.io.{PrintWriter, StringWriter}
-
 import org.scalatest.matchers.should.Matchers
 import viper.silicon.state.Identifier
 import DSL._
+import org.scalatest.BeforeAndAfter
 import org.scalatest.funsuite.AnyFunSuite
+import viper.silicon.Config
 import viper.silicon.state.terms._
+import viper.silicon.verifier.Verifier
 
-class TriggerRewriterTests extends AnyFunSuite with Matchers {
+class TriggerRewriterTests extends AnyFunSuite with Matchers with BeforeAndAfter {
   val dummySink = new PrintWriter(new StringWriter())
 //  val dummyLogger = new MultiRunLogger(dummySink, () => None)
   val counter = new viper.silicon.utils.Counter()
@@ -32,15 +34,20 @@ class TriggerRewriterTests extends AnyFunSuite with Matchers {
     }
   }
 
-  val x0 = Var(Identifier("x0"), sorts.Int)
-  val x1 = Var(Identifier("x1"), sorts.Int)
-  val y0 = Var(Identifier("y0"), sorts.Int)
-  val z0 = Var(Identifier("z0"), sorts.Int)
+  lazy val x0 = Var(Identifier("x0"), sorts.Int)
+  lazy val x1 = Var(Identifier("x1"), sorts.Int)
+  lazy val y0 = Var(Identifier("y0"), sorts.Int)
+  lazy val z0 = Var(Identifier("z0"), sorts.Int)
 
   import rewriter.rewrite
 
+  before {
+    Verifier.config = new Config(Seq())
+  }
+
+
   test("No-ops") {
-    val forall1 = Forall(x, True(), Trigger(f(x)), "forall1")
+    val forall1 = Forall(x, True, Trigger(f(x)), "forall1")
     val forall2 = Forall(x, f(x), Trigger(f(x)), "forall2")
     val forall3 = Forall(Seq(x, y, b), f(x), Trigger(f(x)), "forall3")
 
@@ -51,50 +58,50 @@ class TriggerRewriterTests extends AnyFunSuite with Matchers {
 
   test("Successes") {
     rewrite(
-      Forall(x, x > `0`, Trigger(f(x + n)))
+      Forall(x, x > `0`, Trigger(f(x + n)), "")
     ) should be (Some(
-      Forall(x0, x0 - n > `0`, Trigger(f(x0)))
+      Forall(x0, x0 - n > `0`, Trigger(f(x0)), "")
     ))
 
     rewrite(
-      Forall(x, f(x, x + `1`) > x, Trigger(f(x, x + `1`)))
+      Forall(x, f(x, x + `1`) > x, Trigger(f(x, x + `1`)), "")
     ) should be (Some(
       Forall(Seq(x, x0), /* TODO: Make order of variables predictable (or use an ordered set) */
              (x === x0 - `1`) ==> (f(x, x0) > x),
-             Trigger(f(x, x0)))
+             Trigger(f(x, x0)), "")
     ))
 
     rewrite(
-      Forall(x, f(x + `1`) === g(x - `2`) + f(x), Trigger(Seq(f(x + `1`), g(x - `2`))))
+      Forall(x, f(x + `1`) === g(x - `2`) + f(x), Trigger(Seq(f(x + `1`), g(x - `2`))), "")
     ) should contain oneOf (
       // TODO: Can we make the result deterministic?
       Forall(Seq(x0, x1),
              (x0 - `1` === x1 + `2`) ==> (f(x0) === g(x1) + f(x0 - `1`)),
-             Trigger(Seq(f(x0), g(x1))))
+             Trigger(Seq(f(x0), g(x1))), "")
     ,
       Forall(Seq(x0, x1),
              (x0 - `1` === x1 + `2`) ==> (f(x0) === g(x1) + f(x1 + `2`)),
-             Trigger(Seq(f(x0), g(x1))))
+             Trigger(Seq(f(x0), g(x1))), "")
     )
 
     rewrite(
-      Forall(Seq(x, y, z), f(x, y + `1`) > z, Trigger(g(x, y + `1`, z)))
+      Forall(Seq(x, y, z), f(x, y + `1`) > z, Trigger(g(x, y + `1`, z)), "")
     ) should be (Some(
-      Forall(Seq(x, z, y0), f(x, y0) > z, Trigger(g(x, y0, z)))
+      Forall(Seq(x, z, y0), f(x, y0) > z, Trigger(g(x, y0, z)), "")
     ))
   }
 
   test("Failures") {
     rewrite(
-      Forall(x, True(), Trigger(f(x * n)))
+      Forall(x, True, Trigger(f(x * n)), "")
     ) should be (None) /* Multiplication is currently not handled */
 
     rewrite(
-      Forall(x, True(), Trigger(f(x / n)))
+      Forall(x, True, Trigger(f(x / n)), "")
     ) should be (None) /* Division is currently not handled */
 
     rewrite(
-      Forall(Seq(x, y), True(), Trigger(f(x + y)))
+      Forall(Seq(x, y), True, Trigger(f(x + y)), "")
     ) should be (None) /* Invalid triggers that mention more than one quantified variable are currently not handled */
   }
 }