diff --git a/src/col/vct/col/ast/expr/apply/InstancePredicateApplyImpl.scala b/src/col/vct/col/ast/expr/apply/InstancePredicateApplyImpl.scala
index 9170b22467..efbd6e952f 100644
--- a/src/col/vct/col/ast/expr/apply/InstancePredicateApplyImpl.scala
+++ b/src/col/vct/col/ast/expr/apply/InstancePredicateApplyImpl.scala
@@ -1,6 +1,6 @@
 package vct.col.ast.expr.apply
 
-import vct.col.ast.InstancePredicateApply
+import vct.col.ast.{InstancePredicateApply, WritePerm}
 import vct.col.print.{Ctx, Doc, Group, Precedence, Text}
 import vct.col.ast.ops.InstancePredicateApplyOps
 
diff --git a/src/col/vct/col/ast/expr/apply/PredicateApplyImpl.scala b/src/col/vct/col/ast/expr/apply/PredicateApplyImpl.scala
index 2461e645de..b7cb588bd8 100644
--- a/src/col/vct/col/ast/expr/apply/PredicateApplyImpl.scala
+++ b/src/col/vct/col/ast/expr/apply/PredicateApplyImpl.scala
@@ -1,6 +1,6 @@
 package vct.col.ast.expr.apply
 
-import vct.col.ast.PredicateApply
+import vct.col.ast.{PredicateApply, WritePerm}
 import vct.col.print.{Ctx, Doc, DocUtil, Empty, Group, Precedence, Text}
 import vct.col.ast.ops.PredicateApplyOps
 
diff --git a/src/main/vct/main/modes/VeSUV.scala b/src/main/vct/main/modes/VeSUV.scala
index f460b9281a..ae7e4ad3a0 100644
--- a/src/main/vct/main/modes/VeSUV.scala
+++ b/src/main/vct/main/modes/VeSUV.scala
@@ -14,7 +14,9 @@ case object VeSUV extends LazyLogging {
     val stages = Stages
       .vesuvOfOptions(options, ConstantBlameProvider(collector))
     stages.run(options.inputs) match {
-      case Left(_: UserError) => EXIT_CODE_ERROR
+      case Left(err: UserError) =>
+        logger.error(err.text)
+        EXIT_CODE_ERROR
       case Left(err: SystemError) => throw err
       case Right(()) =>
         logger.info("Transformation complete")
diff --git a/src/main/vct/main/stages/Backend.scala b/src/main/vct/main/stages/Backend.scala
index eccdc2cbdc..dcf00226f9 100644
--- a/src/main/vct/main/stages/Backend.scala
+++ b/src/main/vct/main/stages/Backend.scala
@@ -57,6 +57,7 @@ case object Backend {
               options.siliconPrintQuantifierStats.isDefined,
             reportOnNoProgress = options.devSiliconReportOnNoProgress,
             traceBranchConditions = options.devSiliconTraceBranchConditions,
+            optimizeUnsafe = options.devUnsafeOptimization,
             branchConditionReportInterval =
               options.devSiliconBranchConditionReportInterval,
             options = options.backendFlags,
diff --git a/src/main/vct/main/stages/GenerateRASI.scala b/src/main/vct/main/stages/GenerateRASI.scala
index ee83377001..ad2e8e91f7 100644
--- a/src/main/vct/main/stages/GenerateRASI.scala
+++ b/src/main/vct/main/stages/GenerateRASI.scala
@@ -1,7 +1,24 @@
 package vct.main.stages
 
+import com.typesafe.scalalogging.LazyLogging
+import hre.io.LiteralReadable
 import hre.stages.Stage
-import vct.col.ast.{InstanceField, InstanceMethod, InstancePredicate, Node}
+import vct.col.ast.{
+  Declaration,
+  Deref,
+  Expr,
+  InstanceField,
+  InstanceMethod,
+  InstancePredicate,
+  Node,
+  Predicate,
+  Procedure,
+  Program,
+  Verification,
+  VerificationContext,
+}
+import vct.col.origin.{LabelContext, Origin, PreferredName}
+import vct.col.print.Ctx
 import vct.col.rewrite.Generation
 import vct.options.Options
 import vct.rewrite.rasi.{
@@ -12,16 +29,26 @@ import vct.rewrite.rasi.{
   SizeVariable,
 }
 
-import java.nio.file.Path
+import java.nio.charset.StandardCharsets
+import java.nio.file.{Files, Path}
 
 case object GenerateRASI {
   def ofOptions(options: Options): Stage[Node[_ <: Generation], Unit] = {
-    GenerateRASI(options.vesuvRasiVariables, options.vesuvOutput)
+    GenerateRASI(
+      options.vesuvRasiVariables,
+      options.vesuvRasiSplitVariables,
+      options.vesuvOutput,
+      test = options.vesuvRasiTest,
+    )
   }
 }
 
-case class GenerateRASI(vars: Option[Seq[String]], out: Path)
-    extends Stage[Node[_ <: Generation], Unit] {
+case class GenerateRASI(
+    vars: Option[Seq[String]],
+    split: Option[Seq[String]],
+    out: Path,
+    test: Boolean,
+) extends Stage[Node[_ <: Generation], Unit] with LazyLogging {
 
   override def friendlyName: String =
     "Generate reachable abstract states invariant"
@@ -31,16 +58,65 @@ case class GenerateRASI(vars: Option[Seq[String]], out: Path)
   override def run(in1: Node[_ <: Generation]): Unit = {
     val in = in1.asInstanceOf[Node[Generation]]
     val main_method =
-      in.collectFirst {
-        case m: InstanceMethod[_]
-            if m.o.getPreferredName.get.snake.equals("main") =>
-          m
-      }.get
+      in.collectFirst { case m: Procedure[_] if m.vesuv_entry => m }.get
     val variables: Set[ConcreteVariable[Generation]] =
       vars.getOrElse(Seq()).map(s => resolve_variable(in, s)).toSet
+    val split_on_variables: Option[Set[ConcreteVariable[Generation]]] = split
+      .map(seq => seq.map(s => resolve_variable(in, s)).toSet)
     val parameter_invariant: InstancePredicate[Generation] =
       get_parameter_invariant(in)
-    new RASIGenerator().test(main_method, variables, parameter_invariant, out)
+    if (test) {
+      new RASIGenerator().test(main_method, variables, parameter_invariant, out)
+    } else {
+      val rasis: Seq[(String, Expr[Generation])] = new RASIGenerator().execute(
+        main_method,
+        variables,
+        split_on_variables,
+        parameter_invariant,
+        in,
+      )
+      val predicates: Seq[Predicate[Generation]] = rasis
+        .map(t => rasi_predicate(t._1, t._2))
+      implicit val o: Origin = Origin(Seq(LabelContext("rasi-generation")))
+      val verification: Verification[Generation] = Verification(
+        Seq(VerificationContext(Program(predicates)(o))),
+        Seq(),
+      )
+
+      val name_map: Map[Declaration[_], String] = Map
+        .from(predicates.flatMap(p =>
+          p.collect {
+            case Deref(_, ref) =>
+              ref.decl -> ref.decl.o.getPreferredName.get.snake
+            case p: Predicate[_] => p -> p.o.getPreferredName.get.snake
+          }
+        ))
+      print(verification, name_map)
+    }
+  }
+
+  private def rasi_predicate(
+      name: String,
+      rasi: Expr[Generation],
+  ): Predicate[Generation] = {
+    implicit val o: Origin = Origin(Seq(LabelContext("rasi-generation")))
+      .withContent(PreferredName(Seq(name)))
+    new Predicate(Seq(), Some(rasi), threadLocal = false, inline = true)
+  }
+
+  private def print(
+      in: Verification[_ <: Generation],
+      name_map: Map[Declaration[_], String],
+  ): Unit = {
+    val ctx = Ctx(syntax = Ctx.PVL, names = name_map)
+
+    val buf = new StringBuffer()
+    in.write(buf)(ctx)
+    val path = s"invariant.pvl"
+    val txt = LiteralReadable(path, buf.toString)
+
+    logger.info(s"Writing ${txt.fileName} to $out")
+    Files.write(out, txt.data.getBytes(StandardCharsets.UTF_8))
   }
 
   private def resolve_variable(
diff --git a/src/main/vct/main/stages/Output.scala b/src/main/vct/main/stages/Output.scala
index 734360cb26..e98cdc416c 100644
--- a/src/main/vct/main/stages/Output.scala
+++ b/src/main/vct/main/stages/Output.scala
@@ -2,9 +2,15 @@ package vct.main.stages
 
 import com.typesafe.scalalogging.LazyLogging
 import hre.io.{LiteralReadable, Readable}
-import hre.stages.{Stage, Stages}
-import vct.col.ast.{Declaration, Node, Program, Verification}
-import vct.col.origin.DiagnosticOrigin
+import hre.stages.{FunctionStage, Stage, Stages}
+import vct.col.ast.{
+  Declaration,
+  Node,
+  Program,
+  Verification,
+  VerificationContext,
+}
+import vct.col.origin.{DiagnosticOrigin, Origin}
 import vct.col.print.{Ctx, Namer}
 import vct.col.rewrite.{Generation, InitialGeneration}
 import vct.options.Options
@@ -22,9 +28,19 @@ case object Output {
   def vesuvOfOptions[G <: Generation](
       options: Options
   ): Stages[ParseResult[G], Unit] = {
-//    FunctionStage((pr: ParseResult[_ <: Generation]) => Program(pr.decls)(DiagnosticOrigin)(DiagnosticOrigin))
-//      .thenRun(??? /* Output(options.vesuvOutput, Ctx.PVL) */)
-    ???
+    implicit val o: Origin = DiagnosticOrigin
+    FunctionStage((pr: ParseResult[_ <: Generation]) =>
+      Verification(
+        Seq(VerificationContext(Program(pr.decls)(DiagnosticOrigin))),
+        Seq(),
+      )
+    ).thenRun(Output(
+      Some(options.vesuvOutput),
+      Ctx.PVL,
+      Files.isDirectory(options.vesuvOutput),
+    )).thenRun(FunctionStage((_: Seq[LiteralReadable]) =>
+        ()
+      )) // TODO: Not the prettiest, but I have no time for this. I blame Bob.
   }
 
   def veymontOfOptions(
@@ -63,9 +79,9 @@ case class Output(out: Option[Path], syntax: Ctx.Syntax, splitDecls: Boolean)
 
     val txts: Seq[LiteralReadable] =
       if (splitDecls) {
-        in.asInstanceOf[Program[_]].declarations.zipWithIndex.map {
+        in.tasks.map(t => t.program).flatMap(p => p.declarations).zipWithIndex.map {
           case (decl, i) =>
-            val name = names.getOrElse(decl.asInstanceOf, s"unknown$i")
+            val name = names.getOrElse(decl.asInstanceOf[Declaration[Generation]], s"unknown$i")
             val fileName = s"${name}.${extension(syntax)}"
             val buf = new StringBuffer()
             decl.write(buf)(ctx)
diff --git a/src/main/vct/main/stages/PrintCFG.scala b/src/main/vct/main/stages/PrintCFG.scala
index 4b8d2ef73e..0db7fbcf12 100644
--- a/src/main/vct/main/stages/PrintCFG.scala
+++ b/src/main/vct/main/stages/PrintCFG.scala
@@ -1,7 +1,7 @@
 package vct.main.stages
 
 import hre.stages.Stage
-import vct.col.ast.{InstanceMethod, Node}
+import vct.col.ast.{Node, Procedure}
 import vct.col.rewrite.Generation
 import vct.options.Options
 import vct.rewrite.cfg.CFGPrinter
@@ -21,11 +21,10 @@ case class PrintCFG(out: Path) extends Stage[Node[_ <: Generation], Unit] {
   override def progressWeight: Int = 0
 
   override def run(in1: Node[_ <: Generation]): Unit = {
-    // TODO: Is there a better way to find a "main" method?
     val main_method =
       in1.collectFirst {
-        case m: InstanceMethod[_]
-            if m.o.getPreferredName.get.snake.equals("main") =>
+        case m: Procedure[_]
+            if m.vesuv_entry =>
           m
       }.get
     CFGPrinter().print_ast_as_cfg(main_method, out)
diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala
index b084476a1f..894c9f7d27 100644
--- a/src/main/vct/main/stages/Transformation.scala
+++ b/src/main/vct/main/stages/Transformation.scala
@@ -148,6 +148,7 @@ object Transformation extends LazyLogging {
           bipResults = bipResults,
           splitVerificationByProcedure =
             options.devSplitVerificationByProcedure,
+          optimizeUnsafe = options.devUnsafeOptimization,
           veymontGeneratePermissions = options.veymontGeneratePermissions,
         )
     }
@@ -189,10 +190,14 @@ object Transformation extends LazyLogging {
   *   Execute a handler before/after a pass is executed.
   * @param passes
   *   The list of rewrite passes to execute.
+  * @param optimizeUnsafe
+  *   Flag indicating to not do typechecking in-between passes to save
+  *   performance
   */
 class Transformation(
     val onPassEvent: Seq[PassEventHandler],
     val passes: Seq[RewriterBuilder],
+    val optimizeUnsafe: Boolean = false,
 ) extends Stage[Verification[_ <: Generation], Verification[_ <: Generation]]
     with LazyLogging {
   override def friendlyName: String = "Transformation"
@@ -236,11 +241,12 @@ class Transformation(
           action(passes, Transformation.after, pass.key, result)
         }
 
-        result.tasks.map(_.program)
-          .flatMap(program => program.check.map(program -> _)) match {
-          case Nil => // ok
-          case errors => throw TransformationCheckError(pass, errors)
-        }
+        if (!optimizeUnsafe)
+          result.tasks.map(_.program)
+            .flatMap(program => program.check.map(program -> _)) match {
+            case Nil => // ok
+            case errors => throw TransformationCheckError(pass, errors)
+          }
 
         result = PrettifyBlocks().dispatch(result)
       }
@@ -293,6 +299,7 @@ case class SilverTransformation(
     bipResults: BIP.VerificationResults,
     checkSat: Boolean = true,
     splitVerificationByProcedure: Boolean = false,
+    override val optimizeUnsafe: Boolean = false,
     veymontGeneratePermissions: Boolean = false,
 ) extends Transformation(
       onPassEvent,
@@ -433,6 +440,7 @@ case class SilverTransformation(
         PinSilverNodes,
         Explode.withArg(splitVerificationByProcedure),
       ),
+      optimizeUnsafe = optimizeUnsafe,
     )
 
 case class VeyMontImplementationGeneration(
diff --git a/src/main/vct/options/Options.scala b/src/main/vct/options/Options.scala
index 79e522f5e8..7f4f5f08a1 100644
--- a/src/main/vct/options/Options.scala
+++ b/src/main/vct/options/Options.scala
@@ -244,6 +244,9 @@ case object Options {
         "Indicate, in seconds, the timeout value for the backend verification. If the verification gets stuck " +
           "for longer than this timeout, the verification will timeout."
       ),
+      opt[Unit]("dev-unsafe-optimization").maybeHidden()
+        .action((_, c) => c.copy(devUnsafeOptimization = true))
+        .text("Optimizes runtime at the cost of progress logging and readability of error messages"),
       opt[Path]("dev-silicon-z3-log-file").maybeHidden()
         .action((p, c) => c.copy(devSiliconZ3LogFile = Some(p)))
         .text("Path for z3 to write smt2 log file to"),
@@ -326,11 +329,20 @@ case object Options {
           .action((_, c) => c.copy(vesuvGenerateRasi = true)).text(
             "Instead of transforming a SystemC design to PVL, generate a global invariant for a PVL program"
           ).children(
+            opt[Unit]("rasi-graph-output")
+              .action((_, c) => c.copy(vesuvRasiTest = true)).text(
+                "Output RASI graph to test the algorithm rather than outputting the invariant"
+              ),
             opt[Seq[String]]("rasi-vars").valueName("<var1>,...")
               .action((vars, c) => c.copy(vesuvRasiVariables = Some(vars)))
               .text(
                 "[WIP] Preliminary selection mechanism for RASI variables; might be replaced later"
-              )
+              ),
+            opt[Seq[String]]("split-rasi").valueName("<var1>,...")
+              .action((vars, c) => c.copy(vesuvRasiSplitVariables = Some(vars)))
+              .text(
+                "[WIP] Preliminary selection mechanism for localizing the RASI based on certain variables; might be changed later"
+              ),
           ),
       ),
       note(""),
@@ -433,6 +445,7 @@ case class Options(
     devSiliconTraceBranchConditions: Boolean = false,
     devCarbonBoogieLogFile: Option[Path] = None,
     devViperProverLogFile: Option[Path] = None,
+    devUnsafeOptimization: Boolean = false,
 
     // VeyMont options
     veymontOutput: Option[Path] = None,
@@ -444,7 +457,9 @@ case class Options(
     // VeSUV options
     vesuvOutput: Path = null,
     vesuvGenerateRasi: Boolean = false,
+    vesuvRasiTest: Boolean = false,
     vesuvRasiVariables: Option[Seq[String]] = None,
+    vesuvRasiSplitVariables: Option[Seq[String]] = None,
 
     // Control flow graph options
     cfgOutput: Path = null,
diff --git a/src/parsers/vct/parsers/transform/systemctocol/colmodel/COLSystem.java b/src/parsers/vct/parsers/transform/systemctocol/colmodel/COLSystem.java
index 968ab39b55..018844b9ee 100644
--- a/src/parsers/vct/parsers/transform/systemctocol/colmodel/COLSystem.java
+++ b/src/parsers/vct/parsers/transform/systemctocol/colmodel/COLSystem.java
@@ -31,6 +31,7 @@
 import vct.parsers.transform.systemctocol.exceptions.UnsupportedException;
 import vct.parsers.transform.systemctocol.util.GeneratedBlame;
 import vct.parsers.transform.systemctocol.util.OriGen;
+import vct.parsers.transform.systemctocol.util.Seqs;
 
 import java.util.stream.Collectors;
 
@@ -313,6 +314,11 @@ else if (size_expr instanceof SCVariableExpression var_expr && is_parameter(var_
      */
     private Class<T> main;
 
+    /**
+     * The scheduler method in the Main class.
+     */
+    private InstanceMethod<T> main_method;
+
     /**
      * Global permission invariant.
      */
@@ -553,6 +559,31 @@ public ParseResult<T> to_parse_result() {
                 List.from(CollectionConverters.asScala(expected_errors)));
     }
 
+    public void create_vesuv_entry() {
+        java.util.List<Statement<T>> body = new java.util.ArrayList<>();
+
+        // Create variable of Main class
+        TClass<T> main_type = new TClass<>(new DirectRef<>(main, ClassTag$.MODULE$.apply(Class.class)), Seqs.empty(), OriGen.create());
+        Variable<T> var = new Variable<>(main_type, OriGen.create("design"));
+
+        // Constructor call
+        PVLNew<T> new_expr = new PVLNew<>(main_type, Seqs.empty(), Seqs.empty(), NO_GIVEN, NO_YIELDS, new GeneratedBlame<>(), OriGen.create());
+        Local<T> m_deref = new Local<>(new DirectRef<>(var, ClassTag$.MODULE$.apply(Variable.class)), OriGen.create());
+
+        // main method call
+        Ref<T, InstanceMethod<T>> scheduler_ref = new DirectRef<>(main_method, ClassTag$.MODULE$.apply(InstanceMethod.class));
+        InvokeMethod<T> call_main = new InvokeMethod<>(m_deref, scheduler_ref, NO_EXPRS, NO_EXPRS, NO_TYPES, NO_GIVEN,
+                NO_YIELDS, new GeneratedBlame<>(), OriGen.create());
+
+        body.add(new LocalDecl<>(var, OriGen.create()));
+        body.add(new Assign<>(m_deref, new_expr, new GeneratedBlame<>(), OriGen.create()));
+        body.add(call_main);
+
+        Block<T> block = new Block<>(List.from(CollectionConverters.asScala(body)), OriGen.create());
+
+        global_declarations.add(new VeSUVMainMethod<>(Option.apply(block), new GeneratedBlame<>(), OriGen.create()));
+    }
+
     // ===================================================== //
     // ================ GETTERS AND SETTERS ================ //
     // ===================================================== //
@@ -585,6 +616,15 @@ public Class<T> get_main() {
         return main;
     }
 
+    /**
+     * Registers the main scheduler method.
+     *
+     * @param main_method Scheduler method
+     */
+    public void set_main_method(InstanceMethod<T> main_method) {
+        this.main_method = main_method;
+    }
+
     /**
      * Registers the global permission invariant.
      *
@@ -887,7 +927,7 @@ public void add_function_usage(SCFunction function, ProcessClass proc) {
      * @return A list of process classes that use the given function
      */
     public java.util.List<ProcessClass> get_function_usages(SCFunction function) {
-        return this.function_usages.get(function);
+        return this.function_usages.getOrDefault(function, new java.util.ArrayList<>());
     }
 
     /**
diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java
index 5b34bd3bbd..334575a099 100644
--- a/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java
+++ b/src/parsers/vct/parsers/transform/systemctocol/engine/MainTransformer.java
@@ -115,6 +115,11 @@ public class MainTransformer<T> {
      */
     private InstanceMethod<T> find_minimum_advance;
 
+    /**
+     * Scheduler helper method <code>update_events</code>
+     */
+    private InstanceMethod<T> update_events;
+
     /**
      * Scheduler helper method <code>wakeup_after_wait</code>.
      */
@@ -605,6 +610,7 @@ private void create_helper_methods() {
         immediate_wakeup = create_immediate_wakeup();
         reset_events_no_delta = create_reset_events_no_delta();
         find_minimum_advance = create_find_minimum_advance();
+        update_events = create_update_events();
         wakeup_after_wait = create_wakeup_after_wait();
         reset_all_events = create_reset_all_events();
     }
@@ -806,6 +812,69 @@ private InstanceMethod<T> create_find_minimum_advance() {
                 false, true, new GeneratedBlame<>(), OriGen.create("find_minimum_advance"));
     }
 
+    /**
+     * Creates the abstract helper method <code>update_events</code>. This method takes as a parameter the next time
+     * advance and updates all events based on
+     *
+     * @return An <code>InstanceMethod</code> object encoding the method <code>wakeup_after_wait</code>
+     */
+    private InstanceMethod<T> create_update_events() {
+        // Create parameter
+        Variable<T> param = new Variable<>(col_system.T_INT, OriGen.create("advance"));
+        Ref<T, Variable<T>> param_ref = new DirectRef<>(param, ClassTag$.MODULE$.apply(Variable.class));
+        Local<T> param_deref = new Local<>(param_ref, OriGen.create());
+        List<Variable<T>> params = List.from(CollectionConverters.asScala(java.util.List.of(param)));
+
+        // Create references to the event and process state variables
+        Ref<T, InstanceField<T>> event_state_ref = new DirectRef<>(col_system.get_event_state(), ClassTag$.MODULE$.apply(InstanceField.class));
+        Deref<T> event_state_deref = new Deref<>(col_system.THIS, event_state_ref, new GeneratedBlame<>(), OriGen.create());
+        Ref<T, InstanceField<T>> process_state_ref = new DirectRef<>(col_system.get_process_state(), ClassTag$.MODULE$.apply(InstanceField.class));
+        Deref<T> process_state_deref = new Deref<>(col_system.THIS, process_state_ref, new GeneratedBlame<>(), OriGen.create());
+        Ref<T, InstanceField<T>> prim_update_ref = new DirectRef<>(col_system.get_primitive_channel_update(), ClassTag$.MODULE$.apply(InstanceField.class));
+        Deref<T> prim_update_deref = new Deref<>(col_system.THIS, prim_update_ref, new GeneratedBlame<>(), OriGen.create());
+
+        // Create general permission context
+        Expr<T> context = create_helper_context();
+
+        // Create condition on event state and primitive update sequence
+        Old<T> old_process_state = new Old<>(process_state_deref, Option.empty(), new GeneratedBlame<>(), OriGen.create());
+        Eq<T> event_state_unchanged = new Eq<>(process_state_deref, old_process_state, OriGen.create());
+        Old<T> old_prim_update = new Old<>(prim_update_deref, Option.empty(), new GeneratedBlame<>(), OriGen.create());
+        Eq<T> prim_update_unchanged = new Eq<>(prim_update_deref, old_prim_update, OriGen.create());
+        And<T> unchanged = new And<>(event_state_unchanged, prim_update_unchanged, OriGen.create());
+
+        // Create conditions for the changing state
+        java.util.List<Expr<T>> ensures = new java.util.ArrayList<>();
+        ensures.add(context);
+        ensures.add(unchanged);
+        for(int i = 0; i < col_system.get_total_nr_events(); i++) {
+            // Prepare appropriate sequence accesses
+            SeqSubscript<T> ev_state_i = new SeqSubscript<>(event_state_deref, new IntegerValue<>(BigInt.apply(i), OriGen.create()),
+                    new GeneratedBlame<>(), OriGen.create());
+            Old<T> old_ev_state_i = new Old<>(ev_state_i, Option.empty(), new GeneratedBlame<>(), OriGen.create());
+
+            // Conditions
+            Less<T> event_negative = new Less<>(old_ev_state_i, col_system.MINUS_ONE, OriGen.create());
+            GreaterEq<T> event_positive = new GreaterEq<>(old_ev_state_i, col_system.MINUS_ONE, OriGen.create());
+
+            // Reset (if the event is -2 or -3 before, reset it to -3)
+            Eq<T> event_reset = new Eq<>(ev_state_i, col_system.MINUS_THREE, OriGen.create());
+
+            // Advance (if the event is scheduled before, subtract the given time from it)
+            Minus<T> reduced = new Minus<>(old_ev_state_i, param_deref, OriGen.create());
+            Eq<T> event_reduced = new Eq<>(ev_state_i, reduced, OriGen.create());
+
+            // Add to updates
+            ensures.add(new Implies<>(event_negative, event_reset, OriGen.create()));
+            ensures.add(new Implies<>(event_positive, event_reduced, OriGen.create()));
+        }
+
+        // Generate contract and method and return
+        ApplicableContract<T> contract = col_system.to_applicable_contract(context, col_system.fold_star(ensures));
+        return new InstanceMethod<>(col_system.T_VOID, params, col_system.NO_VARS, col_system.NO_VARS, Option.empty(), contract,
+                false, false, new GeneratedBlame<>(), OriGen.create("update_events"));
+    }
+
     /**
      * Creates the abstract helper method <code>wakeup_after_wait</code>. This method sets the <code>process_state</code>
      * of all processes that are waiting on an event with an <code>event_state</code> of 0 or -1 (i.e. waiting for zero
@@ -1096,21 +1165,16 @@ private Statement<T> create_scheduler_loop_if_body() {
                 col_system.NO_EXPRS, col_system.NO_TYPES, col_system.NO_GIVEN, col_system.NO_YIELDS, new GeneratedBlame<>(), OriGen.create());
         Assign<T> assign_ma = new Assign<>(ma_local, fma_invoke, new GeneratedBlame<>(), OriGen.create());
 
-        // Set min_advance to zero if it is -1
-        Eq<T> cond = new Eq<>(ma_local, col_system.MINUS_ONE, OriGen.create());
+        // Set min_advance to zero if it is less than or equal to -1
+        LessEq<T> cond = new LessEq<>(ma_local, col_system.MINUS_ONE, OriGen.create());
         Assign<T> reset_ma = new Assign<>(ma_local, col_system.ZERO, new GeneratedBlame<>(), OriGen.create());
         java.util.List<Tuple2<Expr<T>, Statement<T>>> branches = java.util.List.of(new Tuple2<>(cond, reset_ma));
         Branch<T> cond_reset_ma = new Branch<>(List.from(CollectionConverters.asScala(branches)), OriGen.create());
 
-        // Advance delays in event_state
-        java.util.List<Expr<T>> literal_values = new java.util.ArrayList<>();
-        for (Expr<T> ev_i : event_entries) {
-            Less<T> condition = new Less<>(ev_i, col_system.MINUS_ONE, OriGen.create());
-            Minus<T> minus = new Minus<>(ev_i, ma_local, OriGen.create());
-            literal_values.add(new Select<>(condition, col_system.MINUS_THREE, minus, OriGen.create()));
-        }
-        LiteralSeq<T> reset_literal = new LiteralSeq<>(col_system.T_INT, List.from(CollectionConverters.asScala(literal_values)), OriGen.create());
-        Assign<T> advance_delays = new Assign<>(event_state_deref, reset_literal, new GeneratedBlame<>(), OriGen.create());
+        // Call update_events
+        Ref<T, InstanceMethod<T>> ue_ref = new DirectRef<>(update_events, ClassTag$.MODULE$.apply(InstanceMethod.class));
+        InvokeMethod<T> call_ue = new InvokeMethod<>(col_system.THIS, ue_ref, List.from(CollectionConverters.asScala(java.util.List.of(ma_local))),
+                col_system.NO_EXPRS, col_system.NO_TYPES, col_system.NO_GIVEN, col_system.NO_YIELDS, new GeneratedBlame<>(), OriGen.create());
 
         // Call wakeup_after_wait
         Ref<T, InstanceMethod<T>> waw_ref = new DirectRef<>(wakeup_after_wait, ClassTag$.MODULE$.apply(InstanceMethod.class));
@@ -1123,7 +1187,7 @@ private Statement<T> create_scheduler_loop_if_body() {
                 col_system.NO_TYPES, col_system.NO_GIVEN, col_system.NO_YIELDS, new GeneratedBlame<>(), OriGen.create());
 
         // Put it all together and return
-        java.util.List<Statement<T>> statements = java.util.List.of(update_phase, declare_ma, assign_ma, cond_reset_ma, advance_delays, call_waw, call_rae);
+        java.util.List<Statement<T>> statements = java.util.List.of(update_phase, declare_ma, assign_ma, cond_reset_ma, call_ue, call_waw, call_rae);
         return new Block<>(List.from(CollectionConverters.asScala(statements)), OriGen.create());
     }
 
@@ -1224,6 +1288,7 @@ private void assemble_main() {
         declarations.add(immediate_wakeup);
         declarations.add(reset_events_no_delta);
         declarations.add(find_minimum_advance);
+        declarations.add(update_events);
         declarations.add(wakeup_after_wait);
         declarations.add(reset_all_events);
 
@@ -1238,5 +1303,6 @@ private void assemble_main() {
         // Register Main class in COL system context
         col_system.add_global_declaration(main_class);
         col_system.set_main(main_class);
+        col_system.set_main_method(scheduler);
     }
 }
diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java
index 1c4d9a4c75..4cfca17cae 100644
--- a/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java
+++ b/src/parsers/vct/parsers/transform/systemctocol/engine/Transformer.java
@@ -73,6 +73,8 @@ public void create_col_model() {
 		transform_classes();
 		// Finish the Main class
 		create_main_class();
+		// Create program entry point
+		create_vesuv_entry();
 	}
 
 	/**
@@ -347,6 +349,10 @@ private void create_main_class() {
 		main_transformer.create_main_class();
 	}
 
+	private void create_vesuv_entry() {
+		col_system.create_vesuv_entry();
+	}
+
 	// ============================================================================================================== //
 	// ============================================= UTILITY FUNCTIONS ============================================== //
 	// ============================================================================================================== //
diff --git a/src/rewrite/vct/rewrite/cfg/CFGGenerator.scala b/src/rewrite/vct/rewrite/cfg/CFGGenerator.scala
index 3b36024824..27797741c8 100644
--- a/src/rewrite/vct/rewrite/cfg/CFGGenerator.scala
+++ b/src/rewrite/vct/rewrite/cfg/CFGGenerator.scala
@@ -14,7 +14,7 @@ case class CFGGenerator[G]() extends LazyLogging {
   private val converted_nodes: mutable.Map[GlobalIndex[G], CFGNode[G]] = mutable
     .HashMap[GlobalIndex[G], CFGNode[G]]()
 
-  def generate(entry: InstanceMethod[G]): CFGNode[G] = {
+  def generate(entry: Procedure[G]): CFGNode[G] = {
     logger.info("Generating control flow graph")
     val res = convert(
       entry.body.get,
diff --git a/src/rewrite/vct/rewrite/cfg/CFGPrinter.scala b/src/rewrite/vct/rewrite/cfg/CFGPrinter.scala
index 27becbc769..112f18efd7 100644
--- a/src/rewrite/vct/rewrite/cfg/CFGPrinter.scala
+++ b/src/rewrite/vct/rewrite/cfg/CFGPrinter.scala
@@ -1,7 +1,7 @@
 package vct.rewrite.cfg
 
 import hre.io.RWFile
-import vct.col.ast.{BooleanValue, Expr, InstanceMethod}
+import vct.col.ast.{BooleanValue, Expr, Procedure}
 import vct.col.origin.Origin
 
 import java.io.Writer
@@ -33,7 +33,7 @@ case class CFGPrinter[G]() {
     writer.append("}")
   }
 
-  def print_ast_as_cfg(entry_point: InstanceMethod[G], path: Path): Unit = {
+  def print_ast_as_cfg(entry_point: Procedure[G], path: Path): Unit = {
     val cfg_root: CFGNode[G] = CFGGenerator().generate(entry_point)
     find_all_nodes(cfg_root)
     RWFile(path).write(w => print_cfg(w))
diff --git a/src/rewrite/vct/rewrite/cfg/Index.scala b/src/rewrite/vct/rewrite/cfg/Index.scala
index f24ad962f3..114d783eda 100644
--- a/src/rewrite/vct/rewrite/cfg/Index.scala
+++ b/src/rewrite/vct/rewrite/cfg/Index.scala
@@ -158,7 +158,7 @@ sealed trait Index[G] {
 object Index {
   def from[G](node: Node[G], index: Int): Index[G] =
     node match {
-      case instance_method: InstanceMethod[G] => InitialIndex(instance_method)
+      case procedure: Procedure[G] => InitialIndex(procedure)
       case run_method: RunMethod[G] => RunMethodIndex(run_method)
       case assign: Assign[G] => AssignmentIndex(assign, index)
       case pvl_branch: PVLBranch[G] => PVLBranchIndex(pvl_branch, index)
@@ -207,7 +207,7 @@ object Index {
 
 // TODO: Handle contract assertions for InitialIndex, RunMethodIndex, FramedProof, RangedForIndex, ???
 
-case class InitialIndex[G](instance_method: InstanceMethod[G])
+case class InitialIndex[G](instance_method: Procedure[G])
     extends Index[G] {
   override def make_step(): Set[(NextIndex[G], Option[Expr[G]])] =
     Set((Outgoing(), None))
diff --git a/src/rewrite/vct/rewrite/rasi/AbstractProcess.scala b/src/rewrite/vct/rewrite/rasi/AbstractProcess.scala
index b2ff5ca6c4..6629422a03 100644
--- a/src/rewrite/vct/rewrite/rasi/AbstractProcess.scala
+++ b/src/rewrite/vct/rewrite/rasi/AbstractProcess.scala
@@ -260,7 +260,8 @@ case class AbstractProcess[G](obj: Expr[G]) {
                 (edges._1.head.target match {
                   case CFGTerminal() => false
                   case target: CFGNode[G] =>
-                    new StaticScanner(target, state).scan_can_change_variables()
+                    new StaticScanner(target, state)
+                      .scan_can_change_variables(None)
                 })
             (
               true,
@@ -324,7 +325,8 @@ case class AbstractProcess[G](obj: Expr[G]) {
     RASISuccessor(
       new_states.deciding_variables ++ enabled_edges._2,
       enabled_edges._1
-        .flatMap(e => new_states.successors.map(s => take_edge(e, s))),
+        .flatMap(e => new_states.successors.map(s => take_edge(e, s)))
+        .flatMap(s => s.split_values()),
     )
   }
 
diff --git a/src/rewrite/vct/rewrite/rasi/AbstractState.scala b/src/rewrite/vct/rewrite/rasi/AbstractState.scala
index 31e1925e8b..62af2eee07 100644
--- a/src/rewrite/vct/rewrite/rasi/AbstractState.scala
+++ b/src/rewrite/vct/rewrite/rasi/AbstractState.scala
@@ -25,6 +25,21 @@ case class AbstractState[G](
     )
   }
 
+  /** Returns a state with the same tracked variables, but with no knowledge of
+    * their values.
+    *
+    * @return
+    *   A copy of this state with all variable values perfectly uncertain
+    */
+  def reset: AbstractState[G] = {
+    AbstractState(
+      valuations.map(v => v._1 -> UncertainValue.uncertain_of(v._1.t)),
+      processes,
+      lock,
+      parameters,
+    )
+  }
+
   /** Updates the state by changing the program counter for a process.
     *
     * @param process
@@ -76,6 +91,22 @@ case class AbstractState[G](
   def unlocked(): AbstractState[G] =
     AbstractState(valuations, processes, None, parameters)
 
+  /** Splits this state such that every variable for which this is possible only
+    * has a single value in any of the resulting states. Variables for which
+    * this is not possible have their uncertain value copied into all substates.
+    *
+    * @return
+    *   A set of states that, in total, represents the same valuations as this
+    *   state, with each resulting state containing only variable valuations
+    *   that are as sharp as possible
+    */
+  def split_values(): Set[AbstractState[G]] = {
+    val valuation_sets: Iterable[Set[(ConcreteVariable[G], UncertainValue)]] =
+      valuations.map(t => t._2.split.getOrElse(Set(t._2)).map(v => t._1 -> v))
+    Utils.cartesian_product(valuation_sets)
+      .map(vs => AbstractState(Map.from(vs), processes, lock, parameters))
+  }
+
   /** Updates the state by adding a path condition to its knowledge of
     * parameters (to avoid infeasible assumptions about potential paths).
     *
@@ -90,7 +121,7 @@ case class AbstractState[G](
     cond match {
       case None => this
       case Some(expr) =>
-        val c =
+        val c: Map[ResolvableVariable[G], UncertainValue] =
           new ConstraintSolver(
             this,
             valuations.keySet
@@ -331,9 +362,21 @@ case class AbstractState[G](
       case Mult(left, right) =>
         resolve_integer_expression(left, is_old, is_contract) *
           resolve_integer_expression(right, is_old, is_contract)
+      case AmbiguousDiv(left, right) =>
+        resolve_integer_expression(left, is_old, is_contract) /
+          resolve_integer_expression(right, is_old, is_contract)
+      case AmbiguousTruncDiv(left, right) => // TODO: Handle this?
+        resolve_integer_expression(left, is_old, is_contract) /
+          resolve_integer_expression(right, is_old, is_contract)
       case FloorDiv(left, right) =>
         resolve_integer_expression(left, is_old, is_contract) /
           resolve_integer_expression(right, is_old, is_contract)
+      case AmbiguousMod(left, right) =>
+        resolve_integer_expression(left, is_old, is_contract) %
+          resolve_integer_expression(right, is_old, is_contract)
+      case AmbiguousTruncMod(left, right) => // TODO: Handle this?
+        resolve_integer_expression(left, is_old, is_contract) %
+          resolve_integer_expression(right, is_old, is_contract)
       case Mod(left, right) =>
         resolve_integer_expression(left, is_old, is_contract) %
           resolve_integer_expression(right, is_old, is_contract)
@@ -467,8 +510,12 @@ case class AbstractState[G](
       case Implies(left, right) =>
         (!resolve_boolean_expression(left, is_old, is_contract)) ||
         resolve_boolean_expression(right, is_old, is_contract)
+      case AmbiguousEq(left, right, _) =>
+        handle_equality(left, right, is_old, is_contract, negate = false)
       case Eq(left, right) =>
         handle_equality(left, right, is_old, is_contract, negate = false)
+      case AmbiguousNeq(left, right, _) =>
+        handle_equality(left, right, is_old, is_contract, negate = true)
       case Neq(left, right) =>
         handle_equality(left, right, is_old, is_contract, negate = true)
       case AmbiguousGreater(left, right) =>
@@ -576,6 +623,7 @@ case class AbstractState[G](
         UncertainBooleanValue.from(true) // TODO: How to handle quantifiers?!
       case Result(_) => UncertainBooleanValue.uncertain()
       case AmbiguousResult() => UncertainBooleanValue.uncertain()
+      case SeqMember(_, _) => UncertainBooleanValue.uncertain() // TODO: Implement something for this?
     }
 
   /** Evaluates a collection expression and returns an uncertain collection
@@ -812,10 +860,15 @@ case class AbstractState[G](
     * @return
     *   An expression that encodes this state
     */
-  def to_expression: Expr[G] = {
+  def to_expression(
+      objs: Option[Map[ConcreteVariable[G], Expr[G]]]
+  ): Expr[G] = {
     val sorted_valuations = valuations.toSeq
       .sortWith((t1, t2) => t1._1.compare(t2._1))
-    sorted_valuations.map(v => v._2.to_expression(v._1.to_expression))
-      .reduce((e1, e2) => And(e1, e2)(e1.o))
+    sorted_valuations.map(v =>
+      v._2.to_expression(
+        v._1.to_expression(Option.when(objs.nonEmpty)(objs.get.apply(v._1)))
+      )
+    ).reduce((e1, e2) => And(e1, e2)(e1.o))
   }
 }
diff --git a/src/rewrite/vct/rewrite/rasi/ConcreteVariable.scala b/src/rewrite/vct/rewrite/rasi/ConcreteVariable.scala
index 67cd0540f1..41366e61a1 100644
--- a/src/rewrite/vct/rewrite/rasi/ConcreteVariable.scala
+++ b/src/rewrite/vct/rewrite/rasi/ConcreteVariable.scala
@@ -66,7 +66,9 @@ sealed trait ConcreteVariable[G] extends ResolvableVariable[G] {
     * @return
     *   A COL expression representing this variable
     */
-  def to_expression: Expr[G]
+  def to_expression(obj: Option[Expr[G]]): Expr[G]
+
+  def get_declaration: Declaration[G]
 
   protected def field_equals(expr: Expr[G], field: InstanceField[G]): Boolean =
     expr match {
@@ -98,12 +100,19 @@ sealed trait ConcreteVariable[G] extends ResolvableVariable[G] {
 case class LocalVariable[G](variable: Variable[G]) extends ConcreteVariable[G] {
   override def is(expr: Expr[G], state: AbstractState[G]): Boolean =
     variable_equals(expr, variable)
+
   override def is_contained_by(
       expr: Expr[G],
       state: AbstractState[G],
   ): Boolean = is(expr, state)
-  override def to_expression: Expr[G] = Local[G](variable.ref)(variable.o)
+
+  override def to_expression(obj: Option[Expr[G]]): Expr[G] =
+    Local[G](variable.ref)(variable.o)
+
+  override def get_declaration: Declaration[G] = variable
+
   override def t: Type[G] = variable.t
+
   override def compare(other: ConcreteVariable[G]): Boolean =
     other match {
       case LocalVariable(v) => v.toInlineString > variable.toInlineString
@@ -117,13 +126,21 @@ case class FieldVariable[G](field: InstanceField[G])
     extends ConcreteVariable[G] {
   override def is(expr: Expr[G], state: AbstractState[G]): Boolean =
     field_equals(expr, field)
+
   override def is_contained_by(
       expr: Expr[G],
       state: AbstractState[G],
   ): Boolean = is(expr, state)
-  override def to_expression: Expr[G] =
-    Deref[G](AmbiguousThis()(field.o), field.ref)(field.o)(field.o)
+
+  override def to_expression(obj: Option[Expr[G]]): Expr[G] =
+    Deref[G](obj.getOrElse(AmbiguousThis()(field.o)), field.ref)(field.o)(
+      field.o
+    )
+
+  override def get_declaration: Declaration[G] = field
+
   override def t: Type[G] = field.t
+
   override def compare(other: ConcreteVariable[G]): Boolean =
     other match {
       case LocalVariable(_) => true
@@ -144,15 +161,21 @@ case class SizeVariable[G](field: InstanceField[G])
       case Size(obj) => field_equals(obj, field)
       case _ => false
     }
+
   override def is_contained_by(
       expr: Expr[G],
       state: AbstractState[G],
   ): Boolean = is(expr, state) || field_equals(expr, field)
-  override def to_expression: Expr[G] =
-    Size(Deref[G](AmbiguousThis()(field.o), field.ref)(field.o)(field.o))(
+
+  override def to_expression(obj: Option[Expr[G]]): Expr[G] =
+    Size(Deref[G](obj.getOrElse(AmbiguousThis()(field.o)), field.ref)(field.o)(
       field.o
-    )
+    ))(field.o)
+
+  override def get_declaration: Declaration[G] = field
+
   override def t: Type[G] = TInt()(field.o)
+
   override def compare(other: ConcreteVariable[G]): Boolean =
     other match {
       case LocalVariable(_) => true
@@ -184,6 +207,7 @@ case class IndexedVariable[G](field: InstanceField[G], i: Int)
           .getOrElse(-1)
       case _ => false
     }
+
   override def is_contained_by(
       expr: Expr[G],
       state: AbstractState[G],
@@ -203,30 +227,41 @@ case class IndexedVariable[G](field: InstanceField[G], i: Int)
           .getOrElse(i - 1) >= i
       case _ => field_equals(expr, field) || is(expr, state)
     }
-  override def to_expression: Expr[G] =
+
+  override def to_expression(obj: Option[Expr[G]]): Expr[G] =
     field.t match {
       case TSeq(_) =>
         SeqSubscript(
-          Deref[G](AmbiguousThis()(field.o), field.ref)(field.o)(field.o),
+          Deref[G](obj.getOrElse(AmbiguousThis()(field.o)), field.ref)(field.o)(
+            field.o
+          ),
           IntegerValue(i)(field.o),
         )(field.o)(field.o)
       case TArray(_) =>
         ArraySubscript(
-          Deref[G](AmbiguousThis()(field.o), field.ref)(field.o)(field.o),
+          Deref[G](obj.getOrElse(AmbiguousThis()(field.o)), field.ref)(field.o)(
+            field.o
+          ),
           IntegerValue(i)(field.o),
         )(field.o)(field.o)
       case TPointer(_) =>
         PointerSubscript(
-          Deref[G](AmbiguousThis()(field.o), field.ref)(field.o)(field.o),
+          Deref[G](obj.getOrElse(AmbiguousThis()(field.o)), field.ref)(field.o)(
+            field.o
+          ),
           IntegerValue(i)(field.o),
         )(field.o)(field.o)
     }
+
+  override def get_declaration: Declaration[G] = field
+
   override def t: Type[G] =
     field.t match {
       case TSeq(element) => element
       case TArray(element) => element
       case TPointer(element) => element
     }
+
   override def compare(other: ConcreteVariable[G]): Boolean =
     other match {
       case LocalVariable(_) => true
diff --git a/src/rewrite/vct/rewrite/rasi/ConstraintMap.scala b/src/rewrite/vct/rewrite/rasi/ConstraintMap.scala
index 1755f0289a..8a90fba22a 100644
--- a/src/rewrite/vct/rewrite/rasi/ConstraintMap.scala
+++ b/src/rewrite/vct/rewrite/rasi/ConstraintMap.scala
@@ -53,7 +53,7 @@ case class ConstraintMap[G](
     *   <code>true</code> if any variable is mapped to an impossible value,
     *   <code>false</code> otherwise
     */
-  def is_impossible: Boolean = resolve.exists(t => t._2.is_impossible)
+  def is_impossible: Boolean = constraints.exists(t => t._2.is_impossible)
 
   /** Checks whether the constraint map is empty. An empty map represents the
     * constraint of all variables to the uncertain value of their respective
@@ -64,8 +64,7 @@ case class ConstraintMap[G](
     *   <code>true</code> if the map does not constrain any variable,
     *   <code>false</code> otherwise
     */
-  def is_empty: Boolean =
-    resolve.forall(t => t._2 == UncertainValue.uncertain_of(t._1.t))
+  def is_empty: Boolean = resolve.forall(v => v._2.is_uncertain)
 }
 case object ConstraintMap {
   def from[G](
diff --git a/src/rewrite/vct/rewrite/rasi/ConstraintSolver.scala b/src/rewrite/vct/rewrite/rasi/ConstraintSolver.scala
index f43b4ef49d..c5c1dc163c 100644
--- a/src/rewrite/vct/rewrite/rasi/ConstraintSolver.scala
+++ b/src/rewrite/vct/rewrite/rasi/ConstraintSolver.scala
@@ -179,8 +179,10 @@ class ConstraintSolver[G](
   ): Set[ConstraintMap[G]] = {
     val pure_left = is_pure(comp.left)
     val pure_right = is_pure(comp.right)
-    if (pure_left == pure_right)
-      return Set(ConstraintMap.empty[G])
+    if (pure_left && pure_right) { return Set(ConstraintMap.empty[G]) }
+    if (!pure_left && !pure_right) {
+      return handle_double_impure_update(comp, negate)
+    }
     // Now, exactly one side is pure, and the other contains a concrete variable
     // Resolve the variable and the other side of the equation
     comp.left.t match {
@@ -190,6 +192,97 @@ class ConstraintSolver[G](
     }
   }
 
+  private def handle_double_impure_update(
+      comp: Comparison[G],
+      negate: Boolean,
+  ): Set[ConstraintMap[G]] =
+    comp.left.t match {
+      case _: IntType[_] | _: TBool[_] =>
+        val left_val: UncertainValue = state.resolve_expression(comp.left)
+        val right_val: UncertainValue = state.resolve_expression(comp.right)
+        if (left_val.is_uncertain && right_val.is_uncertain)
+          Set(ConstraintMap.empty[G])
+        else {
+          comp match {
+            case _: Eq[_] | _: AmbiguousEq[_] =>
+              val value: UncertainValue = left_val.intersection(right_val)
+              if (!negate)
+                Set(
+                  expr_equals(comp.left, value) &&
+                    expr_equals(comp.right, value)
+                )
+              else
+                Set(ConstraintMap.empty[G])
+            case _: Neq[_] | _: AmbiguousNeq[_] =>
+              val value: UncertainValue = left_val.intersection(right_val)
+              if (negate)
+                Set(
+                  expr_equals(comp.left, value) &&
+                    expr_equals(comp.right, value)
+                )
+              else
+                Set(ConstraintMap.empty[G])
+            case _: Greater[_] | _: AmbiguousGreater[_] =>
+              Set(
+                limit_variable(
+                  comp.left,
+                  right_val.asInstanceOf[UncertainIntegerValue],
+                  !negate,
+                  negate,
+                ) && limit_variable(
+                  comp.right,
+                  left_val.asInstanceOf[UncertainIntegerValue],
+                  negate,
+                  negate,
+                )
+              )
+            case _: GreaterEq[_] | _: AmbiguousGreaterEq[_] =>
+              Set(
+                limit_variable(
+                  comp.left,
+                  right_val.asInstanceOf[UncertainIntegerValue],
+                  !negate,
+                  !negate,
+                ) && limit_variable(
+                  comp.right,
+                  left_val.asInstanceOf[UncertainIntegerValue],
+                  negate,
+                  !negate,
+                )
+              )
+            case _: LessEq[_] | _: AmbiguousLessEq[_] =>
+              Set(
+                limit_variable(
+                  comp.left,
+                  right_val.asInstanceOf[UncertainIntegerValue],
+                  negate,
+                  !negate,
+                ) && limit_variable(
+                  comp.right,
+                  left_val.asInstanceOf[UncertainIntegerValue],
+                  !negate,
+                  !negate,
+                )
+              )
+            case _: Less[_] | _: AmbiguousLess[_] =>
+              Set(
+                limit_variable(
+                  comp.left,
+                  right_val.asInstanceOf[UncertainIntegerValue],
+                  negate,
+                  negate,
+                ) && limit_variable(
+                  comp.right,
+                  left_val.asInstanceOf[UncertainIntegerValue],
+                  !negate,
+                  negate,
+                )
+              )
+          }
+        }
+      case _ => Set(ConstraintMap.empty[G]) // TODO: Handle collection values
+    }
+
   private def is_pure(node: Node[G]): Boolean =
     node match {
       // The old value of a variable is always pure, since it cannot be updated
@@ -221,14 +314,14 @@ class ConstraintSolver[G](
         state.resolve_expression(comp.right)
 
     comp match {
-      case _: Eq[_] =>
+      case _: Eq[_] | _: AmbiguousEq[_] =>
         Set(
           if (!negate)
             expr_equals(expr, value)
           else
             expr_equals(expr, value.complement())
         )
-      case _: Neq[_] =>
+      case _: Neq[_] | _: AmbiguousNeq[_] =>
         Set(
           if (!negate)
             expr_equals(expr, value.complement())
@@ -236,33 +329,33 @@ class ConstraintSolver[G](
             expr_equals(expr, value)
         )
       case AmbiguousGreater(_, _) | Greater(_, _) =>
-        limit_variable(
+        Set(limit_variable(
           expr,
           value.asInstanceOf[UncertainIntegerValue],
           pure_left == negate,
           negate,
-        )
+        ))
       case AmbiguousGreaterEq(_, _) | GreaterEq(_, _) =>
-        limit_variable(
+        Set(limit_variable(
           expr,
           value.asInstanceOf[UncertainIntegerValue],
           pure_left == negate,
           !negate,
-        )
+        ))
       case AmbiguousLessEq(_, _) | LessEq(_, _) =>
-        limit_variable(
+        Set(limit_variable(
           expr,
           value.asInstanceOf[UncertainIntegerValue],
           pure_left != negate,
           !negate,
-        )
+        ))
       case AmbiguousLess(_, _) | Less(_, _) =>
-        limit_variable(
+        Set(limit_variable(
           expr,
           value.asInstanceOf[UncertainIntegerValue],
           pure_left != negate,
           negate,
-        )
+        ))
     }
   }
 
@@ -271,17 +364,17 @@ class ConstraintSolver[G](
       b: UncertainIntegerValue,
       var_greater: Boolean,
       can_be_equal: Boolean,
-  ): Set[ConstraintMap[G]] = {
+  ): ConstraintMap[G] = {
     if (var_greater) {
       if (can_be_equal)
-        Set(expr_equals(expr, b.above_eq()))
+        expr_equals(expr, b.above_eq())
       else
-        Set(expr_equals(expr, b.above()))
+        expr_equals(expr, b.above())
     } else {
       if (can_be_equal)
-        Set(expr_equals(expr, b.below_eq()))
+        expr_equals(expr, b.below_eq())
       else
-        Set(expr_equals(expr, b.below()))
+        expr_equals(expr, b.below())
     }
   }
 
@@ -352,8 +445,10 @@ class ConstraintSolver[G](
     val update_map = index_update_map ++ size_update_map
 
     comp match {
-      case _: Eq[_] if !negate => Set(ConstraintMap.from_cons(update_map))
-      case _: Neq[_] if negate => Set(ConstraintMap.from_cons(update_map))
+      case _: Eq[_] | _: AmbiguousEq[_] if !negate =>
+        Set(ConstraintMap.from_cons(update_map))
+      case _: Neq[_] | _: AmbiguousNeq[_] if negate =>
+        Set(ConstraintMap.from_cons(update_map))
       case _ =>
         throw new IllegalArgumentException(
           s"The operator ${comp.toInlineString} is not supported for collections"
diff --git a/src/rewrite/vct/rewrite/rasi/Interval.scala b/src/rewrite/vct/rewrite/rasi/Interval.scala
index e86df9def7..56d8a85370 100644
--- a/src/rewrite/vct/rewrite/rasi/Interval.scala
+++ b/src/rewrite/vct/rewrite/rasi/Interval.scala
@@ -108,6 +108,7 @@ sealed abstract class Interval {
   def unary_- : Interval
   def pow(other: Interval): Interval
   def sub_intervals(): Set[Interval] = Set(this)
+  def values: Option[Set[Int]]
   def try_to_resolve(): Option[Int]
   def to_expression[G](variable: Expr[G]): Expr[G] // TODO: Use proper origin
 }
@@ -127,6 +128,7 @@ case object EmptyInterval extends Interval {
   override def %(other: Interval): Interval = this
   override def unary_- : Interval = this
   override def pow(other: Interval): Interval = this
+  override def values: Option[Set[Int]] = Some(Set.empty[Int])
   override def try_to_resolve(): Option[Int] = None
   override def to_expression[G](variable: Expr[G]): Expr[G] =
     BooleanValue(value = false)(variable.o)
@@ -232,6 +234,15 @@ case class MultiInterval(intervals: Set[Interval]) extends Interval {
   override def sub_intervals(): Set[Interval] =
     intervals.flatMap(i => i.sub_intervals())
 
+  override def values: Option[Set[Int]] = {
+    intervals.map(i => i.values).reduce((o1, o2) =>
+      if (o1.isEmpty || o2.isEmpty)
+        None
+      else
+        Some(o1.get ++ o2.get)
+    )
+  }
+
   override def try_to_resolve(): Option[Int] = {
     if (intervals.count(i => i != EmptyInterval) == 1)
       intervals.filter(i => i != EmptyInterval).head.try_to_resolve()
@@ -240,7 +251,9 @@ case class MultiInterval(intervals: Set[Interval]) extends Interval {
   }
 
   override def to_expression[G](variable: Expr[G]): Expr[G] = {
-    intervals.map(i => i.to_expression(variable))
+    val sorted: Seq[Interval] = merge_intersecting(intervals).toSeq
+      .sortWith((i1, i2) => i1.below_max().is_subset_of(i2.below_max()))
+    sorted.map(i => i.to_expression(variable))
       .reduce((e1, e2) => Or(e1, e2)(variable.o))
   }
 }
@@ -408,6 +421,8 @@ case class BoundedInterval(lower: Int, upper: Int) extends Interval {
           LowerBoundedInterval(0)
     }
 
+  override def values: Option[Set[Int]] = Some(lower.to(upper).toSet)
+
   override def try_to_resolve(): Option[Int] = {
     if (lower == upper)
       Some(upper)
@@ -518,6 +533,8 @@ case class LowerBoundedInterval(lower: Int) extends Interval {
 
   override def pow(other: Interval): Interval = ???
 
+  override def values: Option[Set[Int]] = None
+
   override def try_to_resolve(): Option[Int] = None
 
   override def to_expression[G](variable: Expr[G]): Expr[G] =
@@ -616,6 +633,8 @@ case class UpperBoundedInterval(upper: Int) extends Interval {
 
   override def pow(other: Interval): Interval = ???
 
+  override def values: Option[Set[Int]] = None
+
   override def try_to_resolve(): Option[Int] = None
 
   override def to_expression[G](variable: Expr[G]): Expr[G] =
@@ -664,6 +683,7 @@ case object UnboundedInterval extends Interval {
     }
   override def unary_- : Interval = this
   override def pow(other: Interval): Interval = this
+  override def values: Option[Set[Int]] = None
   override def try_to_resolve(): Option[Int] = None
   override def to_expression[G](variable: Expr[G]): Expr[G] =
     BooleanValue(value = true)(variable.o)
diff --git a/src/rewrite/vct/rewrite/rasi/RASIConnection.scala b/src/rewrite/vct/rewrite/rasi/RASIConnection.scala
index fea92d4f64..b8b1ab9e3f 100644
--- a/src/rewrite/vct/rewrite/rasi/RASIConnection.scala
+++ b/src/rewrite/vct/rewrite/rasi/RASIConnection.scala
@@ -10,7 +10,8 @@ case class RASISuccessor[G](
 case object RASISuccessor {
   def from[G](successors: Iterable[RASISuccessor[G]]): RASISuccessor[G] =
     RASISuccessor(
-      successors.flatMap(s => s.deciding_variables).toSet,
+      successors.filter(s => s.successors.size > 1)
+        .flatMap(s => s.deciding_variables).toSet,
       successors.flatMap(s => s.successors).toSet,
     )
 }
diff --git a/src/rewrite/vct/rewrite/rasi/RASIGenerator.scala b/src/rewrite/vct/rewrite/rasi/RASIGenerator.scala
index e7471cbf1a..5d22fb101c 100644
--- a/src/rewrite/vct/rewrite/rasi/RASIGenerator.scala
+++ b/src/rewrite/vct/rewrite/rasi/RASIGenerator.scala
@@ -2,15 +2,22 @@ package vct.rewrite.rasi
 
 import com.typesafe.scalalogging.LazyLogging
 import vct.col.ast.{
+  AmbiguousThis,
+  BooleanValue,
+  Class,
+  Declaration,
   Deref,
   Expr,
   InstanceField,
-  InstanceMethod,
   InstancePredicate,
+  Node,
   Null,
   Or,
+  Procedure,
+  TClass,
 }
 import vct.col.origin.Origin
+import vct.col.print.Ctx
 import vct.rewrite.cfg.{CFGEntry, CFGGenerator}
 
 import java.nio.file.Path
@@ -26,18 +33,22 @@ class RASIGenerator[G] extends LazyLogging {
     .ArrayBuffer()
 
   def execute(
-      entry_point: InstanceMethod[G],
+      entry_point: Procedure[G],
       vars: Set[ConcreteVariable[G]],
+      split_on: Option[Set[ConcreteVariable[G]]],
       parameter_invariant: InstancePredicate[G],
-  ): Expr[G] =
+      program: Node[G],
+  ): Seq[(String, Expr[G])] =
     generate_rasi(
       CFGGenerator().generate(entry_point),
       vars,
+      split_on,
       parameter_invariant,
+      program,
     )
 
   def test(
-      entry_point: InstanceMethod[G],
+      entry_point: Procedure[G],
       vars: Set[ConcreteVariable[G]],
       parameter_invariant: InstancePredicate[G],
       out_path: Path,
@@ -52,15 +63,110 @@ class RASIGenerator[G] extends LazyLogging {
   private def generate_rasi(
       node: CFGEntry[G],
       vars: Set[ConcreteVariable[G]],
+      split_on: Option[Set[ConcreteVariable[G]]],
       parameter_invariant: InstancePredicate[G],
-  ): Expr[G] = {
+      program: Node[G],
+  ): Seq[(String, Expr[G])] = {
     explore(node, vars, parameter_invariant)
-    val distinct_states = found_states.distinctBy(s => s.valuations)
-    logger.debug(s"${distinct_states.size} distinct states found")
-    distinct_states.map(s => s.to_expression)
+    val distinct: Int = found_states.distinctBy(s => s.valuations).size
+    logger.info(s"$distinct distinct states found")
+
+    if (split_on.isEmpty)
+      return Seq((
+        "reachable_abstract_states_invariant",
+        get_rasi_expression(_ => true, None, program),
+      ))
+
+    val all_processes: Set[AbstractProcess[G]] = found_states.toSet
+      .flatMap((s: AbstractState[G]) => s.processes.keySet)
+
+    var res: Seq[(String, Expr[G])] = Seq((
+      "interleaving_states",
+      get_rasi_expression(s => s.lock.isEmpty, None, program),
+    ))
+
+    get_var_value_pairs(split_on.get).foreach(t =>
+      res =
+        res :+
+          (
+            get_rasi_name(t._1, t._2),
+            get_rasi_expression(
+              s => s.valuations(t._1) == t._2,
+              Some(get_associated_process(t._1, all_processes)),
+              program,
+            ),
+          )
+    )
+
+    res
+  }
+
+  private def get_associated_process(
+      of: ConcreteVariable[G],
+      from: Set[AbstractProcess[G]],
+  ): AbstractProcess[G] = {
+    from.filter(p => p.obj.t.isInstanceOf[TClass[G]]).collectFirst {
+      case p @ AbstractProcess(obj)
+          if obj.t.asInstanceOf[TClass[G]].cls.decl.decls
+            .contains(of.get_declaration) =>
+        p
+    }.get
+  }
+
+  private def get_rasi_expression(
+      f: AbstractState[G] => Boolean,
+      proc: Option[AbstractProcess[G]],
+      program: Node[G],
+  ): Expr[G] = {
+    val rasi_states = found_states.filter(f)
+      .filter(s => proc.isEmpty || s.lock.isEmpty || s.lock.get == proc.get)
+      .distinctBy(s => s.valuations)
+
+    if (rasi_states.isEmpty)
+      return BooleanValue(value = false)(program.o)
+
+    val objs: Map[ConcreteVariable[G], Expr[G]] = find_fitting_objects(
+      program,
+      rasi_states.head.valuations.keySet,
+    )
+    rasi_states.map(s => s.to_expression(Some(objs)))
       .reduce((e1, e2) => Or(e1, e2)(e1.o))
   }
 
+  private def get_var_value_pairs(
+      split_on_vars: Set[ConcreteVariable[G]]
+  ): Set[(ConcreteVariable[G], UncertainValue)] =
+    split_on_vars.flatMap(v => found_states.map(s => v -> s.valuations(v)))
+
+  private def get_rasi_name(
+      variable: ConcreteVariable[G],
+      value: UncertainValue,
+  ): String = {
+    // Compute variable name
+    val name_map: Map[Declaration[_], String] = Map.from(Seq(
+      variable.get_declaration ->
+        variable.get_declaration.o.getPreferredName.get.snake
+    ))
+    implicit val context: Ctx = Ctx(syntax = Ctx.PVL, names = name_map)
+    val var_name: String = variable.to_expression(None).toStringWithContext
+      .replace("]", "").replace("[", "").replace("this.", "")
+
+    // Compute value string
+    val value_string: String =
+      value match {
+        case i: UncertainIntegerValue =>
+          i.try_to_resolve()
+            .getOrElse(throw new IllegalStateException("Value must be defined"))
+            .toString
+        case b: UncertainBooleanValue =>
+          b.try_to_resolve()
+            .getOrElse(throw new IllegalStateException("Value must be defined"))
+            .toString
+      }
+
+    "rasi_" + var_name + "_" + value_string
+  }
+
   private def print_state_space(
       node: CFGEntry[G],
       vars: Set[ConcreteVariable[G]],
@@ -69,7 +175,7 @@ class RASIGenerator[G] extends LazyLogging {
   ): Unit = {
     explore(node, vars, parameter_invariant)
     val (ns, es) = reduce_redundant_states()
-    logger.debug(s"${ns.size} distinct states found")
+    logger.info(s"${ns.size} distinct states found")
     Utils.print(ns, es, out_path)
   }
 
@@ -79,19 +185,17 @@ class RASIGenerator[G] extends LazyLogging {
       parameter_invariant: InstancePredicate[G],
   ): Unit = {
     logger.info("Starting RASI generation")
-    val start_time: Long = System.nanoTime()
-    var last_measurement: Long = start_time
+    val global_start_time: Long = System.nanoTime()
 
-    val initial_state = AbstractState(
-      get_initial_values(vars),
-      HashMap((AbstractProcess[G](Null()(Origin(Seq()))), node)),
-      None,
-      get_parameter_constraints(parameter_invariant),
-    ).with_condition(parameter_invariant.body)
-
-    found_states += initial_state
-    current_branches += initial_state
+    var considered_variables: Set[ConcreteVariable[G]] = vars
 
+    var generation_start_time: Long = reset(
+      node,
+      considered_variables,
+      parameter_invariant,
+    )
+    var last_measurement_time: Long = generation_start_time
+    var initial_state: AbstractState[G] = current_branches.head
     var i = 0
 
     while (current_branches.nonEmpty) {
@@ -99,25 +203,54 @@ class RASIGenerator[G] extends LazyLogging {
       current_branches -= curr
 
       val successor: RASISuccessor[G] = curr.successors()
-      found_edges.addAll(successor.edges(curr))
-      successor.successors.foreach(s =>
-        if (!found_states.contains(s)) {
-          found_states += s; current_branches += s
+
+      if (successor.deciding_variables.nonEmpty) {
+        val time: Long =
+          (System.nanoTime() - generation_start_time) / 1_000_000L
+        logger.info(
+          s"Found relevant new variables; abort generation [$i iterations in ${time}ms]"
+        )
+        val found_vars: Seq[String] = successor.deciding_variables.toSeq
+          .sortWith((v1, v2) => v1.compare(v2))
+          .map(v => v.to_expression(None).toInlineString)
+        logger.debug(s"Variables found: $found_vars")
+
+        considered_variables ++= successor.deciding_variables
+
+        generation_start_time = reset(
+          node,
+          considered_variables,
+          parameter_invariant,
+        )
+        last_measurement_time = generation_start_time
+        initial_state = current_branches.head
+        i = 0
+      } else {
+        found_edges.addAll(successor.edges(curr))
+        successor.successors.foreach(s =>
+          if (!found_states.contains(s)) {
+            found_states += s
+            current_branches += s
+          }
+        )
+        i = i + 1
+        if (System.nanoTime() - last_measurement_time > 1_000_000_000L) {
+          last_measurement_time = System.nanoTime()
+          val time =
+            (last_measurement_time - generation_start_time) / 1_000_000L
+          logger.debug(s"[Runtime ${time}ms] Iteration $i: ${found_states
+              .size} states found, ${current_branches.size} yet to explore")
         }
-      )
-      i = i + 1
-      if (System.nanoTime() - last_measurement > 5_000_000_000L) {
-        last_measurement = System.nanoTime()
-        val time = (last_measurement - start_time) / 1_000_000L
-        logger.debug(s"[Runtime ${time}ms] Iteration $i: ${found_states
-            .size} states found, ${current_branches.size} yet to explore")
       }
     }
 
-    val total_time: Long = (System.nanoTime() - start_time) / 1_000_000L
-    logger.info(s"RASI generation complete [$i iterations in ${total_time}ms]")
-
-    // TODO: Detect which variable overapproximations are detrimental to the state space and which are not
+    val current_time: Long = System.nanoTime()
+    val generation_time: Long =
+      (current_time - generation_start_time) / 1_000_000L
+    val total_time: Long = (System.nanoTime() - global_start_time) / 1_000_000L
+    logger
+      .info(s"RASI generation complete [$i iterations in ${generation_time}ms]")
+    logger.info(s"Total runtime: ${total_time}ms")
 
     // The initial state converts to simply "true", so it would make the RASI trivial
     found_states.filterInPlace(s => s.valuations != initial_state.valuations)
@@ -134,6 +267,28 @@ class RASIGenerator[G] extends LazyLogging {
     )
   }
 
+  private def reset(
+      node: CFGEntry[G],
+      vars: Set[ConcreteVariable[G]],
+      parameter_invariant: InstancePredicate[G],
+  ): Long = {
+    found_states.clear()
+    found_edges.clear()
+    current_branches.clear()
+
+    val initial_state = AbstractState(
+      get_initial_values(vars),
+      HashMap((AbstractProcess[G](Null()(Origin(Seq()))), node)),
+      None,
+      get_parameter_constraints(parameter_invariant),
+    ).with_condition(parameter_invariant.body)
+
+    found_states += initial_state
+    current_branches += initial_state
+
+    System.nanoTime()
+  }
+
   private def get_initial_values(
       vars: Set[ConcreteVariable[G]]
   ): Map[ConcreteVariable[G], UncertainValue] = {
@@ -155,12 +310,12 @@ class RASIGenerator[G] extends LazyLogging {
   private def reduce_redundant_states()
       : (Seq[AbstractState[G]], Seq[(AbstractState[G], AbstractState[G])]) = {
     val state_groups: Map[Expr[G], mutable.ArrayBuffer[AbstractState[G]]] = Map
-      .from(found_states.groupBy(s => s.to_expression))
+      .from(found_states.groupBy(s => s.to_expression(None)))
     val edge_groups: Seq[(AbstractState[G], AbstractState[G])] = Seq
       .from(found_edges.map(e =>
         (
-          state_groups(e.from.to_expression).head,
-          state_groups(e.to.to_expression).head,
+          state_groups(e.from.to_expression(None)).head,
+          state_groups(e.to.to_expression(None)).head,
         )
       ))
     (
@@ -168,4 +323,52 @@ class RASIGenerator[G] extends LazyLogging {
       edge_groups.distinct.filter(t => t._1 != t._2),
     )
   }
+
+  private def find_fitting_objects(
+      program: Node[G],
+      vars: Set[ConcreteVariable[G]],
+  ): Map[ConcreteVariable[G], Expr[G]] = {
+    var m: Map[ConcreteVariable[G], Expr[G]] = Map
+      .empty[ConcreteVariable[G], Expr[G]]
+
+    val classes: Seq[Class[G]] = program.collect[Class[G]] { case c: Class[G] =>
+      c
+    }
+    // TODO: Find differently, e.g. with lock invariant?
+    val main_class: Class[G] =
+      classes.find(c => c.o.getPreferredName.get.camel.startsWith("main")).get
+
+    for (v <- vars) {
+      v match {
+        case IndexedVariable(f, _) =>
+          m += (v -> find_field_object(classes, main_class, f))
+        case FieldVariable(f) =>
+          m += (v -> find_field_object(classes, main_class, f))
+        case SizeVariable(f) =>
+          m += (v -> find_field_object(classes, main_class, f))
+        case LocalVariable(f) => m += (v -> AmbiguousThis()(f.o))
+      }
+    }
+
+    m
+  }
+
+  private def find_field_object(
+      classes: Seq[Class[G]],
+      main: Class[G],
+      field: InstanceField[G],
+  ): Expr[G] = {
+    val type_class: Class[G] = classes.find(c => c.decls.contains(field)).get
+    if (type_class == main)
+      return AmbiguousThis()(field.o)
+
+    val obj: InstanceField[G] =
+      main.decls.collectFirst {
+        case f: InstanceField[G]
+            if f.t.isInstanceOf[TClass[G]] &&
+              f.t.asInstanceOf[TClass[G]].cls.decl == type_class =>
+          f
+      }.get
+    Deref[G](AmbiguousThis()(field.o), obj.ref)(field.o)(field.o)
+  }
 }
diff --git a/src/rewrite/vct/rewrite/rasi/StaticScanner.scala b/src/rewrite/vct/rewrite/rasi/StaticScanner.scala
index 918e9e2182..9dbd608c17 100644
--- a/src/rewrite/vct/rewrite/rasi/StaticScanner.scala
+++ b/src/rewrite/vct/rewrite/rasi/StaticScanner.scala
@@ -6,17 +6,19 @@ import vct.rewrite.cfg.{CFGEntry, CFGNode}
 import scala.collection.mutable
 
 class StaticScanner[G](initial_node: CFGNode[G], state: AbstractState[G]) {
-  private val explored_nodes: mutable.Set[CFGEntry[G]] = mutable.Set
+  private val var_change_explored_nodes: mutable.Set[CFGEntry[G]] = mutable.Set
     .empty[CFGEntry[G]]
 
-  def scan_can_change_variables(): Boolean = {
+  def scan_can_change_variables(until: Option[CFGNode[G]]): Boolean = {
+    if (until.nonEmpty)
+      var_change_explored_nodes.add(until.get)
     scan_for_var_changes_from_node(initial_node)
   }
 
   private def scan_for_var_changes_from_node(node: CFGNode[G]): Boolean = {
-    if (explored_nodes.contains(node))
+    if (var_change_explored_nodes.contains(node))
       return false
-    explored_nodes.add(node)
+    var_change_explored_nodes.add(node)
     node_changes_vars(node) || node.successors.map(e => e.target).collect {
       case n: CFGNode[G] => n
     }.exists(n => scan_for_var_changes_from_node(n))
@@ -62,8 +64,8 @@ class StaticScanner[G](initial_node: CFGNode[G], state: AbstractState[G]) {
       // If it is a collection, an update might only change other indices than those tracked
       // Therefore: evaluate the assignment explicitly to see if it affects the tracked variables      TODO: Consider arrays
       case _: TSeq[_] =>
-        state.to_expression != state.with_updated_collection(target, value)
-          .to_expression
+        state.reset.to_expression(None) !=
+          state.reset.with_updated_collection(target, value).to_expression(None)
     }
   }
 
@@ -73,7 +75,8 @@ class StaticScanner[G](initial_node: CFGNode[G], state: AbstractState[G]) {
     if (potential_successor.successors.size != 1)
       true
     else
-      state.to_expression != potential_successor.successors.head.to_expression
+      state.to_expression(None) !=
+        potential_successor.successors.head.to_expression(None)
   }
 
   private def postcondition_changes_vars(
@@ -85,6 +88,7 @@ class StaticScanner[G](initial_node: CFGNode[G], state: AbstractState[G]) {
     if (potential_successor.successors.size != 1)
       true
     else
-      state.to_expression != potential_successor.successors.head.to_expression
+      state.to_expression(None) !=
+        potential_successor.successors.head.to_expression(None)
   }
 }
diff --git a/src/rewrite/vct/rewrite/rasi/UncertainValue.scala b/src/rewrite/vct/rewrite/rasi/UncertainValue.scala
index b5c9dd70e8..b0e79eee9e 100644
--- a/src/rewrite/vct/rewrite/rasi/UncertainValue.scala
+++ b/src/rewrite/vct/rewrite/rasi/UncertainValue.scala
@@ -6,6 +6,7 @@ import vct.col.ast.{BooleanValue, Expr, IntType, Not, TBool, TInt, Type}
 trait UncertainValue {
   def can_be_equal(other: UncertainValue): Boolean
   def can_be_unequal(other: UncertainValue): Boolean
+  def is_uncertain: Boolean
   def is_impossible: Boolean
   def is_subset_of(other: UncertainValue): Boolean
   def complement(): UncertainValue
@@ -15,6 +16,7 @@ trait UncertainValue {
   def ==(other: UncertainValue): UncertainBooleanValue
   def !=(other: UncertainValue): UncertainBooleanValue
   def t[G]: Type[G]
+  def split: Option[Set[UncertainValue]]
 }
 case object UncertainValue {
   def uncertain_of(t: Type[_]): UncertainValue =
@@ -43,6 +45,8 @@ case class UncertainBooleanValue(can_be_true: Boolean, can_be_false: Boolean)
       case _ => true
     }
 
+  override def is_uncertain: Boolean = can_be_true && can_be_false
+
   override def is_impossible: Boolean = !can_be_true && !can_be_false
 
   override def is_subset_of(other: UncertainValue): Boolean =
@@ -99,6 +103,19 @@ case class UncertainBooleanValue(can_be_true: Boolean, can_be_false: Boolean)
 
   override def t[G]: Type[G] = TBool[G]()
 
+  override def split: Option[Set[UncertainValue]] = {
+    if (is_impossible)
+      None
+    else {
+      var res: Set[UncertainValue] = Set.empty[UncertainValue]
+      if (can_be_true)
+        res += UncertainBooleanValue.from(true)
+      if (can_be_false)
+        res += UncertainBooleanValue.from(false)
+      Some(res)
+    }
+  }
+
   def try_to_resolve(): Option[Boolean] = {
     if (can_be_true && !can_be_false)
       Some(true)
@@ -159,6 +176,8 @@ case class UncertainIntegerValue(value: Interval) extends UncertainValue {
       case _ => true
     }
 
+  override def is_uncertain: Boolean = value == UnboundedInterval
+
   override def is_impossible: Boolean = value.empty()
 
   override def is_subset_of(other: UncertainValue): Boolean =
@@ -210,6 +229,12 @@ case class UncertainIntegerValue(value: Interval) extends UncertainValue {
 
   override def t[G]: Type[G] = TInt[G]()
 
+  override def split: Option[Set[UncertainValue]] =
+    value.values match {
+      case None => None
+      case Some(ints) => Some(ints.map(i => UncertainIntegerValue.single(i)))
+    }
+
   def try_to_resolve(): Option[Int] = value.try_to_resolve()
 
   def below_eq(): UncertainIntegerValue =
@@ -284,6 +309,7 @@ case class UncertainSequence(
       )
     )
       return UncertainBooleanValue.from(false)
+
     val length: Option[Int] = len.try_to_resolve()
     val other_length: Option[Int] = other.len.try_to_resolve()
     if (
diff --git a/src/rewrite/vct/rewrite/rasi/Utils.scala b/src/rewrite/vct/rewrite/rasi/Utils.scala
index 0d1eb82300..3121a0c427 100644
--- a/src/rewrite/vct/rewrite/rasi/Utils.scala
+++ b/src/rewrite/vct/rewrite/rasi/Utils.scala
@@ -54,6 +54,24 @@ case object Utils {
   def prod_min(a1: Int, a2: Int, b1: Int, b2: Int): Int =
     Seq(a1 * b1, a1 * b2, a2 * b1, a2 * b2).min
 
+  /** Computes the cartesian product of an arbitrary number of input sequences.
+    *
+    * @param inputs
+    *   A collection containing all inputs for the cartesian product
+    * @tparam T
+    *   Element type of the input sets
+    * @return
+    *   Set of ordered sequences with one element for each input set
+    */
+  def cartesian_product[T](inputs: Iterable[Set[T]]): Set[Seq[T]] = {
+    if (inputs.isEmpty)
+      Set.empty[Seq[T]]
+    else if (inputs.size == 1)
+      inputs.head.map(v => Seq(v))
+    else
+      inputs.head.flatMap(e => cartesian_product(inputs.tail).map(s => e +: s))
+  }
+
   /** Transforms a loop contract to an invariant, if possible.
     *
     * @param contract
@@ -183,7 +201,7 @@ case object Utils {
         node_names,
         edges,
         w,
-        states.head.to_expression.toInlineString.length > 100,
+        states.head.to_expression(None).toInlineString.length > 100,
       )
     )
   }
@@ -200,9 +218,9 @@ case object Utils {
         if (shorten_labels)
           t._2
         else
-          t._1.to_expression.toInlineString
+          t._1.to_expression(None).toInlineString
       ).append(s"${"\""}];${if (shorten_labels)
-          s" /* ${t._1.to_expression.toInlineString} */"
+          s" /* ${t._1.to_expression(None).toInlineString} */"
         else
           ""}\n")
     )
diff --git a/src/rewrite/vct/rewrite/rasi/VariableSelector.scala b/src/rewrite/vct/rewrite/rasi/VariableSelector.scala
index b4bf389233..a1925cce55 100644
--- a/src/rewrite/vct/rewrite/rasi/VariableSelector.scala
+++ b/src/rewrite/vct/rewrite/rasi/VariableSelector.scala
@@ -53,7 +53,6 @@ class VariableSelector[G](initial_state: AbstractState[G]) {
 
     val constraints: Seq[Set[ConstraintMap[G]]] = conditions.toSeq
       .map(e => satisfying_valuations(initial_state, e))
-      .filter(s => s.exists(m => !m.is_empty))
     if (constraints.isEmpty)
       Set.empty[ConcreteVariable[G]]
     else
@@ -87,7 +86,10 @@ class VariableSelector[G](initial_state: AbstractState[G]) {
       case _: IntType[_] | _: TBool[_] | _: TResource[_] =>
         expr match {
           case d @ Deref(_, ref) =>
-            if (state.valuations.exists(t => t._1.is_contained_by(d, state)))
+            if (
+              (state.valuations ++ state.parameters)
+                .exists(t => t._1.is_contained_by(d, state))
+            )
               Set()
             else
               Set(FieldVariable(ref.decl))
@@ -134,7 +136,7 @@ class VariableSelector[G](initial_state: AbstractState[G]) {
         }
       val index: Option[Int] = state.resolve_integer_expression(subscript)
         .try_to_resolve()
-      if (index.isEmpty)
+      if (index.isEmpty || index.get < 0)
         Set()
       else
         Set(IndexedVariable(field, index.get))
diff --git a/src/viper/viper/api/backend/silicon/Silicon.scala b/src/viper/viper/api/backend/silicon/Silicon.scala
index 0fd0ab0b6e..8235358e97 100644
--- a/src/viper/viper/api/backend/silicon/Silicon.scala
+++ b/src/viper/viper/api/backend/silicon/Silicon.scala
@@ -39,6 +39,7 @@ case class Silicon(
     printQuantifierStatistics: Boolean = false,
     reportOnNoProgress: Boolean = true,
     traceBranchConditions: Boolean = false,
+    optimizeUnsafe: Boolean = false,
     branchConditionReportInterval: Option[Int] = Some(1000),
     timeoutValue: Int = 30,
     totalTimeOut: Int = 0,
@@ -96,8 +97,9 @@ case class Silicon(
       z3Path.toString,
       "--z3ConfigArgs",
       z3Config,
-      "--ideModeAdvanced",
     )
+    if (optimizeUnsafe) siliconConfig ++= Seq("--parallelizeBranches")
+    else siliconConfig ++= Seq("--ideModeAdvanced")
 
     if (proverLogFile.isDefined) {
       // PB: note: enableTempDirectory works unexpectedly: it only enables the logging of smtlib provers and does
@@ -121,7 +123,7 @@ case class Silicon(
     siliconConfig :+= "-"
 
     silicon.parseCommandLine(siliconConfig)
-    silicon.symbExLog = SiliconLogListener(
+    if (!optimizeUnsafe) silicon.symbExLog = SiliconLogListener(
       reportOnNoProgress,
       traceBranchConditions,
       branchConditionReportInterval,