diff --git a/conjure_oxide/build.rs b/conjure_oxide/build.rs
index 7566f1ae53..b180af0cb5 100644
--- a/conjure_oxide/build.rs
+++ b/conjure_oxide/build.rs
@@ -22,7 +22,7 @@ fn main() -> io::Result<()> {
                 let stems: Vec<String> = read_dir(subdir.path())?
                     .filter_map(Result::ok)
                     .filter(|entry| {
-                        entry.path().extension().map_or(false, |ext| {
+                        entry.path().extension().is_some_and(|ext| {
                             ext == "essence" || ext == "eprime" || ext == "disabled"
                         })
                     })
@@ -38,7 +38,7 @@ fn main() -> io::Result<()> {
                 let exts: Vec<String> = read_dir(subdir.path())?
                     .filter_map(Result::ok)
                     .filter(|entry| {
-                        entry.path().extension().map_or(false, |ext| {
+                        entry.path().extension().is_some_and(|ext| {
                             ext == "essence" || ext == "eprime" || ext == "disabled"
                         })
                     })
@@ -61,7 +61,7 @@ fn main() -> io::Result<()> {
                         entry
                             .path()
                             .extension()
-                            .map_or(false, |ext| ext == "essence" || ext == "eprime")
+                            .is_some_and(|ext| ext == "essence" || ext == "eprime")
                     })
                     .filter_map(|entry| {
                         entry
@@ -78,7 +78,7 @@ fn main() -> io::Result<()> {
                         entry
                             .path()
                             .extension()
-                            .map_or(false, |ext| ext == "essence" || ext == "eprime")
+                            .is_some_and(|ext| ext == "essence" || ext == "eprime")
                     })
                     .filter_map(|entry| {
                         entry
diff --git a/conjure_oxide/src/main.rs b/conjure_oxide/src/main.rs
index e8559b2b30..082480c99d 100644
--- a/conjure_oxide/src/main.rs
+++ b/conjure_oxide/src/main.rs
@@ -7,11 +7,9 @@ use std::sync::Arc;
 use anyhow::Result as AnyhowResult;
 use anyhow::{anyhow, bail};
 use clap::{arg, command, Parser};
-use conjure_core::ast::pretty::pretty_expressions_as_top_level;
 use conjure_core::rule_engine::rewrite_naive;
 use conjure_oxide::defaults::get_default_rule_sets;
 use schemars::schema_for;
-use serde_json::json;
 use serde_json::to_string_pretty;
 
 use conjure_core::context::Context;
@@ -181,14 +179,14 @@ pub fn main() -> AnyhowResult<()> {
         .init();
 
     if target_family != SolverFamily::Minion {
-        log::error!("Only the Minion solver is currently supported!");
+        tracing::error!("Only the Minion solver is currently supported!");
         exit(1);
     }
 
     let rule_sets = match resolve_rule_sets(target_family, &extra_rule_sets) {
         Ok(rs) => rs,
         Err(e) => {
-            log::error!("Error resolving rule sets: {}", e);
+            tracing::error!("Error resolving rule sets: {}", e);
             exit(1);
         }
     };
@@ -200,7 +198,7 @@ pub fn main() -> AnyhowResult<()> {
         .join(", ");
 
     println!("Enabled rule sets: [{}]", pretty_rule_sets);
-    log::info!(
+    tracing::info!(
         target: "file",
         "Rule sets: {}",
         pretty_rule_sets
@@ -209,14 +207,14 @@ pub fn main() -> AnyhowResult<()> {
     let rule_priorities = get_rule_priorities(&rule_sets)?;
     let rules_vec = get_rules_vec(&rule_priorities);
 
-    log::info!(target: "file",
+    tracing::info!(target: "file",
          "Rules and priorities: {}",
          rules_vec.iter()
             .map(|rule| format!("{}: {}", rule.name, rule_priorities.get(rule).unwrap_or(&0)))
             .collect::<Vec<_>>()
             .join(", "));
 
-    log::info!(target: "file", "Input file: {}", cli.input_file.display());
+    tracing::info!(target: "file", "Input file: {}", cli.input_file.display());
     let input_file: &str = cli.input_file.to_str().ok_or(anyhow!(
         "Given input_file could not be converted to a string"
     ))?;
@@ -252,30 +250,29 @@ pub fn main() -> AnyhowResult<()> {
     context.write().unwrap().file_name = Some(cli.input_file.to_str().expect("").into());
 
     if cfg!(feature = "extra-rule-checks") {
-        log::info!("extra-rule-checks: enabled");
+        tracing::info!("extra-rule-checks: enabled");
     } else {
-        log::info!("extra-rule-checks: disabled");
+        tracing::info!("extra-rule-checks: disabled");
     }
 
     let mut model = model_from_json(&astjson, context.clone())?;
 
-    log::info!(target: "file", "Initial model: {}", json!(model));
+    tracing::info!("Initial model: \n{}\n", model);
 
-    log::info!(target: "file", "Rewriting model...");
+    tracing::info!("Rewriting model...");
 
     if cli.use_optimising_rewriter {
-        log::info!(target: "file", "Using the dirty-clean rewriter...");
+        tracing::info!("Using the dirty-clean rewriter...");
         model = rewrite_model(&model, &rule_sets)?;
     } else {
-        log::info!(target: "file", "Rewriting model...");
+        tracing::info!("Rewriting model...");
         model = rewrite_naive(&model, &rule_sets, false)?;
     }
 
-    let constraints_string = pretty_expressions_as_top_level(&model.constraints);
-    tracing::info!(constraints=%constraints_string, model=%json!(model),"Rewritten model");
+    tracing::info!("Rewritten model: \n{}\n", model);
 
     let solutions = get_minion_solutions(model, cli.number_of_solutions)?; // ToDo we need to properly set the solver adaptor here, not hard code minion
-    log::info!(target: "file", "Solutions: {}", minion_solutions_to_json(&solutions));
+    tracing::info!(target: "file", "Solutions: {}", minion_solutions_to_json(&solutions));
 
     let solutions_json = minion_solutions_to_json(&solutions);
     let solutions_str = to_string_pretty(&solutions_json)?;
diff --git a/conjure_oxide/src/utils/essence_parser.rs b/conjure_oxide/src/utils/essence_parser.rs
index 820873cb0e..d0544e7512 100644
--- a/conjure_oxide/src/utils/essence_parser.rs
+++ b/conjure_oxide/src/utils/essence_parser.rs
@@ -13,8 +13,7 @@ use crate::utils::conjure::EssenceParseError;
 use conjure_core::context::Context;
 use conjure_core::metadata::Metadata;
 use conjure_core::Model;
-use std::collections::BTreeSet;
-use std::collections::HashMap;
+use std::collections::{BTreeMap, BTreeSet};
 
 pub fn parse_essence_file_native(
     path: &str,
@@ -72,7 +71,7 @@ fn get_tree(path: &str, filename: &str, extension: &str) -> (Tree, String) {
 fn parse_find_statement(
     find_statement_list: Node,
     source_code: &str,
-) -> HashMap<Name, DecisionVariable> {
+) -> BTreeMap<Name, DecisionVariable> {
     let mut symbol_table = SymbolTable::new();
 
     for find_statement in named_children(&find_statement_list) {
diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs
index ece99086c9..421ad1d3c3 100644
--- a/conjure_oxide/tests/generated_tests.rs
+++ b/conjure_oxide/tests/generated_tests.rs
@@ -177,7 +177,7 @@ fn integration_test_inner(
     // Stage 1: Read the essence file and check that the model is parsed correctly
     let model = parse_essence_file(path, essence_base, extension, context.clone())?;
     if verbose {
-        println!("Parsed model: {:#?}", model)
+        println!("Parsed model: {}", model)
     }
 
     context.as_ref().write().unwrap().file_name =
@@ -186,7 +186,7 @@ fn integration_test_inner(
     save_model_json(&model, path, essence_base, "parse", accept)?;
     let expected_model = read_model_json(path, essence_base, "expected", "parse")?;
     if verbose {
-        println!("Expected model: {:#?}", expected_model)
+        println!("Expected model: {}", expected_model)
     }
 
     assert_eq!(model, expected_model);
@@ -202,10 +202,21 @@ fn integration_test_inner(
     // } else {
     //     rewrite_model(&model, &rule_sets)?
     // };
+
+    tracing::trace!(
+        target: "rule_engine_human",
+        "Model before rewriting:\n\n{}\n--\n",
+        model
+    );
     let model = rewrite_naive(&model, &rule_sets, false)?;
 
+    tracing::trace!(
+        target: "rule_engine_human",
+        "Final model:\n\n{}",
+        model
+    );
     if verbose {
-        println!("Rewritten model: {:#?}", model)
+        println!("Rewritten model: {}", model)
     }
 
     save_model_json(&model, path, essence_base, "rewrite", accept)?;
@@ -223,7 +234,7 @@ fn integration_test_inner(
 
     let expected_model = read_model_json(path, essence_base, "expected", "rewrite")?;
     if verbose {
-        println!("Expected model: {:#?}", expected_model)
+        println!("Expected model: {}", expected_model)
     }
 
     assert_eq!(model, expected_model);
diff --git a/conjure_oxide/tests/integration/basic/bool/01/bool-01-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/bool/01/bool-01-expected-rule-trace-human.txt
index e69de29bb2..2ee71ea9af 100644
--- a/conjure_oxide/tests/integration/basic/bool/01/bool-01-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/bool/01/bool-01-expected-rule-trace-human.txt
@@ -0,0 +1,18 @@
+Model before rewriting:
+
+find x: bool
+
+such that
+
+
+
+--
+
+Final model:
+
+find x: bool
+
+such that
+
+
+
diff --git a/conjure_oxide/tests/integration/basic/bool/02/bool-02-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/bool/02/bool-02-expected-rule-trace-human.txt
index e69de29bb2..85f15deffa 100644
--- a/conjure_oxide/tests/integration/basic/bool/02/bool-02-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/bool/02/bool-02-expected-rule-trace-human.txt
@@ -0,0 +1,20 @@
+Model before rewriting:
+
+find x: bool
+find y: bool
+
+such that
+
+
+
+--
+
+Final model:
+
+find x: bool
+find y: bool
+
+such that
+
+
+
diff --git a/conjure_oxide/tests/integration/basic/bool/03/bool-03-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/bool/03/bool-03-expected-rule-trace-human.txt
index e69de29bb2..7161b003ed 100644
--- a/conjure_oxide/tests/integration/basic/bool/03/bool-03-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/bool/03/bool-03-expected-rule-trace-human.txt
@@ -0,0 +1,20 @@
+Model before rewriting:
+
+find x: bool
+find y: bool
+
+such that
+
+(x != y)
+
+--
+
+Final model:
+
+find x: bool
+find y: bool
+
+such that
+
+(x != y)
+
diff --git a/conjure_oxide/tests/integration/basic/bool/04/bool-04-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/bool/04/bool-04-expected-rule-trace-human.txt
index e69de29bb2..aef3f0e34f 100644
--- a/conjure_oxide/tests/integration/basic/bool/04/bool-04-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/bool/04/bool-04-expected-rule-trace-human.txt
@@ -0,0 +1,24 @@
+Model before rewriting:
+
+find x: bool
+find y: bool
+find z: int(42)
+
+such that
+
+(x = true),
+(y != false)
+
+--
+
+Final model:
+
+find x: bool
+find y: bool
+find z: int(42)
+
+such that
+
+(x = true),
+(y != false)
+
diff --git a/conjure_oxide/tests/integration/basic/div/01/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/01/input-expected-rule-trace-human.txt
index ce1815dbfc..8757470ea7 100644
--- a/conjure_oxide/tests/integration/basic/div/01/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/div/01/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+
+such that
+
+(UnsafeDiv(a, b) = 1)
+
+--
+
 UnsafeDiv(a, b), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(a, b) @ (b != 0)} 
@@ -28,3 +39,12 @@ DivEq(a, b, 1)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+
+such that
+
+And([DivEq(a, b, 1), (b != 0)])
+
diff --git a/conjure_oxide/tests/integration/basic/div/02/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/02/input-expected-rule-trace-human.txt
index 3547c57afb..0e97d91b28 100644
--- a/conjure_oxide/tests/integration/basic/div/02/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/div/02/input-expected-rule-trace-human.txt
@@ -1,3 +1,13 @@
+Model before rewriting:
+
+find a: int(0..3)
+
+such that
+
+(a >= UnsafeDiv(4, 2))
+
+--
+
 UnsafeDiv(4, 2), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 2 
@@ -10,3 +20,11 @@ Ineq(2, a, 0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+
+such that
+
+Ineq(2, a, 0)
+
diff --git a/conjure_oxide/tests/integration/basic/div/03/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/03/input-expected-rule-trace-human.txt
index 6947221db2..cdab6f8d62 100644
--- a/conjure_oxide/tests/integration/basic/div/03/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/div/03/input-expected-rule-trace-human.txt
@@ -1,3 +1,13 @@
+Model before rewriting:
+
+find a: int(0..9)
+
+such that
+
+(2 = UnsafeDiv(8, a))
+
+--
+
 UnsafeDiv(8, a), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(8, a) @ (a != 0)} 
@@ -28,3 +38,11 @@ DivEq(8, a, 2)
 
 --
 
+Final model:
+
+find a: int(0..9)
+
+such that
+
+And([DivEq(8, a, 2), (a != 0)])
+
diff --git a/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt
index 1fe80055d5..307ee877ae 100644
--- a/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+
+such that
+
+Not((a = UnsafeDiv(b, c)))
+
+--
+
 UnsafeDiv(b, c), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(b, c) @ (c != 0)} 
@@ -55,3 +67,15 @@ DivEq(b, c, __0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+find __0: int(0..3)
+
+such that
+
+Or([(a != __0), (c = 0)]),
+DivEq(b, c, __0)
+
diff --git a/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt
index f8d725ff33..061f3c09e4 100644
--- a/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+
+such that
+
+(a != UnsafeDiv(b, c))
+
+--
+
 UnsafeDiv(b, c), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(b, c) @ (c != 0)} 
@@ -37,3 +49,15 @@ DivEq(b, c, __0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+find __0: int(0..3)
+
+such that
+
+And([(a != __0), (c != 0)]),
+DivEq(b, c, __0)
+
diff --git a/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt
index 1fe80055d5..307ee877ae 100644
--- a/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+
+such that
+
+Not((a = UnsafeDiv(b, c)))
+
+--
+
 UnsafeDiv(b, c), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(b, c) @ (c != 0)} 
@@ -55,3 +67,15 @@ DivEq(b, c, __0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+find __0: int(0..3)
+
+such that
+
+Or([(a != __0), (c = 0)]),
+DivEq(b, c, __0)
+
diff --git a/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt
index 37f8b25afb..38672fe83e 100644
--- a/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt
@@ -1,3 +1,13 @@
+Model before rewriting:
+
+find a: int(0..3)
+
+such that
+
+(Max([2, a]) <= 2)
+
+--
+
 Max([2, a]), 
    ~~> max_to_var ([("Base", 6000)]) 
 __0 
@@ -27,3 +37,15 @@ Ineq(a, __0, 0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find __0: int(2..3)
+
+such that
+
+Ineq(__0, 2, 0),
+Ineq(2, __0, 0),
+Ineq(a, __0, 0),
+Or([(__0 = 2), (__0 = a)])
+
diff --git a/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt
index 474f3c1d09..ade8815dce 100644
--- a/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find a: int(1..3)
+find b: int(1..3)
+
+such that
+
+(Min([a, b]) >= 3)
+
+--
+
 Min([a, b]), 
    ~~> min_to_var ([("Base", 6000)]) 
 __0 
@@ -27,3 +38,16 @@ Ineq(__0, b, 0)
 
 --
 
+Final model:
+
+find a: int(1..3)
+find b: int(1..3)
+find __0: int(1..3)
+
+such that
+
+Ineq(3, __0, 0),
+Ineq(__0, a, 0),
+Ineq(__0, b, 0),
+Or([(__0 = a), (__0 = b)])
+
diff --git a/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt
index 93569bc03e..8529e58e01 100644
--- a/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find a: int(1..3)
+find b: int(1..3)
+
+such that
+
+(Min([a, b]) <= 2)
+
+--
+
 Min([a, b]), 
    ~~> min_to_var ([("Base", 6000)]) 
 __0 
@@ -27,3 +38,16 @@ Ineq(__0, b, 0)
 
 --
 
+Final model:
+
+find a: int(1..3)
+find b: int(1..3)
+find __0: int(1..3)
+
+such that
+
+Ineq(__0, 2, 0),
+Ineq(__0, a, 0),
+Ineq(__0, b, 0),
+Or([(__0 = a), (__0 = b)])
+
diff --git a/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt
index 93569bc03e..eb00d6760e 100644
--- a/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find a: int(1..3)
+find b: int(2..4)
+
+such that
+
+(Min([a, b]) <= 2)
+
+--
+
 Min([a, b]), 
    ~~> min_to_var ([("Base", 6000)]) 
 __0 
@@ -27,3 +38,16 @@ Ineq(__0, b, 0)
 
 --
 
+Final model:
+
+find a: int(1..3)
+find b: int(2..4)
+find __0: int(1..3)
+
+such that
+
+Ineq(__0, 2, 0),
+Ineq(__0, a, 0),
+Ineq(__0, b, 0),
+Or([(__0 = a), (__0 = b)])
+
diff --git a/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt
index 362928f78d..414f5b080f 100644
--- a/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find a: int(1..2)
+find b: int(4..7)
+
+such that
+
+(Min([a, b]) >= 3)
+
+--
+
 Min([a, b]), 
    ~~> min_to_var ([("Base", 6000)]) 
 __0 
@@ -27,3 +38,16 @@ Ineq(__0, b, 0)
 
 --
 
+Final model:
+
+find a: int(1..2)
+find b: int(4..7)
+find __0: int(1..2)
+
+such that
+
+Ineq(3, __0, 0),
+Ineq(__0, a, 0),
+Ineq(__0, b, 0),
+Or([(__0 = a), (__0 = b)])
+
diff --git a/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt
index 47c0b71b99..9b6d90e94f 100644
--- a/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find a: int(1..5)
+find b: int(2..4)
+
+such that
+
+(Min([a, b]) <= 2)
+
+--
+
 Min([a, b]), 
    ~~> min_to_var ([("Base", 6000)]) 
 __0 
@@ -27,3 +38,16 @@ Ineq(__0, b, 0)
 
 --
 
+Final model:
+
+find a: int(1..5)
+find b: int(2..4)
+find __0: int(1..4)
+
+such that
+
+Ineq(__0, 2, 0),
+Ineq(__0, a, 0),
+Ineq(__0, b, 0),
+Or([(__0 = a), (__0 = b)])
+
diff --git a/conjure_oxide/tests/integration/basic/mod/01/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/01/input-expected-rule-trace-human.txt
index 84caa41d86..37165ad9e6 100644
--- a/conjure_oxide/tests/integration/basic/mod/01/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/mod/01/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+
+such that
+
+(a % b = 1)
+
+--
+
 a % b, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(a,b) @ (b != 0)} 
@@ -28,3 +39,12 @@ ModEq(a, b, 1)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+
+such that
+
+And([ModEq(a, b, 1), (b != 0)])
+
diff --git a/conjure_oxide/tests/integration/basic/mod/02/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/02/input-expected-rule-trace-human.txt
index bcea4def68..fbf561494c 100644
--- a/conjure_oxide/tests/integration/basic/mod/02/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/mod/02/input-expected-rule-trace-human.txt
@@ -1,3 +1,13 @@
+Model before rewriting:
+
+find a: int(0..3)
+
+such that
+
+(a >= 4 % 2)
+
+--
+
 4 % 2, 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 0 
@@ -10,3 +20,11 @@ Ineq(0, a, 0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+
+such that
+
+Ineq(0, a, 0)
+
diff --git a/conjure_oxide/tests/integration/basic/mod/03/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/03/input-expected-rule-trace-human.txt
index 220b0ae1c7..e3998d610c 100644
--- a/conjure_oxide/tests/integration/basic/mod/03/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/mod/03/input-expected-rule-trace-human.txt
@@ -1,3 +1,13 @@
+Model before rewriting:
+
+find a: int(0..9)
+
+such that
+
+(2 = 8 % a)
+
+--
+
 8 % a, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(8,a) @ (a != 0)} 
@@ -28,3 +38,11 @@ ModEq(8, a, 2)
 
 --
 
+Final model:
+
+find a: int(0..9)
+
+such that
+
+And([ModEq(8, a, 2), (a != 0)])
+
diff --git a/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt
index 0ea861b307..a663fdf320 100644
--- a/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+
+such that
+
+Not((a = b % c))
+
+--
+
 b % c, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(b,c) @ (c != 0)} 
@@ -55,3 +67,15 @@ ModEq(b, c, __0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+find __0: int(0..2)
+
+such that
+
+Or([(a != __0), (c = 0)]),
+ModEq(b, c, __0)
+
diff --git a/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt
index dc51925f76..98deb9ba20 100644
--- a/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+
+such that
+
+(a != b % c)
+
+--
+
 b % c, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(b,c) @ (c != 0)} 
@@ -37,3 +49,15 @@ ModEq(b, c, __0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+find __0: int(0..2)
+
+such that
+
+And([(a != __0), (c != 0)]),
+ModEq(b, c, __0)
+
diff --git a/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt
index 0ea861b307..a663fdf320 100644
--- a/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+
+such that
+
+Not((a = b % c))
+
+--
+
 b % c, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(b,c) @ (c != 0)} 
@@ -55,3 +67,15 @@ ModEq(b, c, __0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+find __0: int(0..2)
+
+such that
+
+Or([(a != __0), (c = 0)]),
+ModEq(b, c, __0)
+
diff --git a/conjure_oxide/tests/integration/basic/neg/01-negeq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/01-negeq/input-expected-rule-trace-human.txt
index 4170bd5e8a..b6a90befa3 100644
--- a/conjure_oxide/tests/integration/basic/neg/01-negeq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/01-negeq/input-expected-rule-trace-human.txt
@@ -1,6 +1,26 @@
+Model before rewriting:
+
+find x: int(1..2)
+find y: int(-1..1)
+
+such that
+
+(x = -(y))
+
+--
+
 (x = -(y)), 
    ~~> introduce_minuseq_from_eq ([("Minion", 4400)]) 
 MinusEq(x,y) 
 
 --
 
+Final model:
+
+find x: int(1..2)
+find y: int(-1..1)
+
+such that
+
+MinusEq(x,y)
+
diff --git a/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt
index 8802c76f30..59a38fffdc 100644
--- a/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(1..2)
+find y: int(-1..1)
+find z: int(-1..1)
+
+such that
+
+(x = UnsafeDiv(-(y), z))
+
+--
+
 UnsafeDiv(-(y), z), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(-(y), z) @ (z != 0)} 
@@ -43,3 +55,15 @@ DivEq(__0, z, x)
 
 --
 
+Final model:
+
+find x: int(1..2)
+find y: int(-1..1)
+find z: int(-1..1)
+find __0: int(-1..1)
+
+such that
+
+And([DivEq(__0, z, x), (z != 0)]),
+MinusEq(__0,y)
+
diff --git a/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt
index 9ba27d94b8..fac461436e 100644
--- a/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(1..2)
+find y: int(-1..1)
+find z: int(-1..1)
+
+such that
+
+(x = -(UnsafeDiv(y, z)))
+
+--
+
 UnsafeDiv(y, z), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(y, z) @ (z != 0)} 
@@ -49,3 +61,15 @@ DivEq(y, z, __0)
 
 --
 
+Final model:
+
+find x: int(1..2)
+find y: int(-1..1)
+find z: int(-1..1)
+find __0: int(-1..1)
+
+such that
+
+And([MinusEq(x,__0), (z != 0)]),
+DivEq(y, z, __0)
+
diff --git a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt
index 3a5103505b..34d86bbb44 100644
--- a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(1..3)
+find y: int(-1..1)
+find z: int(-1..1)
+
+such that
+
+(x = UnsafeDiv(-(UnsafeDiv(y, z)), z))
+
+--
+
 UnsafeDiv(y, z), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(y, z) @ (z != 0)} 
@@ -100,3 +112,17 @@ DivEq(y, z, __1)
 
 --
 
+Final model:
+
+find x: int(1..3)
+find y: int(-1..1)
+find z: int(-1..1)
+find __0: int(-1..1)
+find __1: int(-1..1)
+
+such that
+
+And([DivEq(__0, z, x), (z != 0), (z != 0)]),
+MinusEq(__0,__1),
+DivEq(y, z, __1)
+
diff --git a/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt
index 15122b5970..538170342c 100644
--- a/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(1..3)
+find y: int(-1..1)
+find z: int(-1..1)
+
+such that
+
+(x = Sum([-(y), z]))
+
+--
+
 Sum([-(y), z]), 
    ~~> flatten_vecop ([("Minion", 4200)]) 
 Sum([__0, z]) 
@@ -31,3 +43,15 @@ SumGeq([__0, z], x)
 
 --
 
+Final model:
+
+find x: int(1..3)
+find y: int(-1..1)
+find z: int(-1..1)
+find __0: int(-1..1)
+
+such that
+
+And([SumLeq([__0, z], x), SumGeq([__0, z], x)]),
+MinusEq(__0,y)
+
diff --git a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt
index 7aa94c79cb..19fb2450aa 100644
--- a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt
@@ -1,3 +1,17 @@
+Model before rewriting:
+
+find a: int(-1..1)
+find b: int(-1..1)
+find x: int(1..3)
+find y: int(-1..1)
+find z: int(-1..1)
+
+such that
+
+(x = Sum([Sum([-(y), -((Sum([z, 1]) - a))]), b]))
+
+--
+
 Sum([Sum([-(y), -((Sum([z, 1]) - a))]), b]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Sum([-(y), -((Sum([z, 1]) - a)), b]) 
@@ -81,3 +95,19 @@ SumGeq([__0, __1, -1, a, b], x)
 
 --
 
+Final model:
+
+find a: int(-1..1)
+find b: int(-1..1)
+find x: int(1..3)
+find y: int(-1..1)
+find z: int(-1..1)
+find __0: int(-1..1)
+find __1: int(-1..1)
+
+such that
+
+And([SumLeq([__0, __1, -1, a, b], x), SumGeq([__0, __1, -1, a, b], x)]),
+MinusEq(__0,y),
+MinusEq(__1,z)
+
diff --git a/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt
index e0ea5e2128..2c75cd55bc 100644
--- a/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(2..4)
+find y: int(2..4)
+find z: int(2..4)
+
+such that
+
+(Product([Product([x, y]), z]) < 15)
+
+--
+
 Product([Product([x, y]), z]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Product([x, y, z]) 
@@ -40,3 +52,17 @@ Ineq(__0, 14, 0)
 
 --
 
+Final model:
+
+find x: int(2..4)
+find y: int(2..4)
+find z: int(2..4)
+find __0: int(8..64)
+find __1: int(4..16)
+
+such that
+
+Ineq(__0, 14, 0),
+FlatProductEq(z,__1,__0),
+FlatProductEq(y,x,__1)
+
diff --git a/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt
index e2b8446903..5d6e45afd0 100644
--- a/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt
@@ -1,3 +1,17 @@
+Model before rewriting:
+
+find a: int(1)
+find b: int(1)
+find c: int(1)
+find d: int(1)
+find e: int(1)
+
+such that
+
+(Sum([a, Sum([b, Sum([c, d])]), e]) = 5)
+
+--
+
 Sum([a, Sum([b, Sum([c, d])]), e]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Sum([a, b, c, d, e]) 
@@ -22,3 +36,15 @@ SumGeq([a, b, c, d, e], 5)
 
 --
 
+Final model:
+
+find a: int(1)
+find b: int(1)
+find c: int(1)
+find d: int(1)
+find e: int(1)
+
+such that
+
+And([SumLeq([a, b, c, d, e], 5), SumGeq([a, b, c, d, e], 5)])
+
diff --git a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt
index e082f61288..3b136688d1 100644
--- a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt
@@ -1,3 +1,16 @@
+Model before rewriting:
+
+find a: int(3..5)
+find x: int(3..4)
+find y: int(1..5)
+find z: int(2..5)
+
+such that
+
+(UnsafeDiv(Sum([Sum([x, y]), z]), a) = 3)
+
+--
+
 Sum([Sum([x, y]), z]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Sum([x, y, z]) 
@@ -61,3 +74,16 @@ SumGeq([x, y, z], __0)
 
 --
 
+Final model:
+
+find a: int(3..5)
+find x: int(3..4)
+find y: int(1..5)
+find z: int(2..5)
+find __0: int(6..14)
+
+such that
+
+And([DivEq(__0, a, 3), (a != 0)]),
+And([SumLeq([x, y, z], __0), SumGeq([x, y, z], __0)])
+
diff --git a/conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/input-expected-rule-trace-human.txt
index ac0d179be9..6d40c59b33 100644
--- a/conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(2..4)
+find y: int(2..4)
+find z: int(2..4)
+
+such that
+
+(Sum([Sum([Product([2, x]), Product([3, y])]), z]) < 14)
+
+--
+
 Sum([Sum([Product([2, x]), Product([3, y])]), z]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Sum([Product([2, x]), Product([3, y]), z]) 
@@ -22,3 +34,13 @@ FlatWeightedSumLeq([2, 3, 1],[x, y, z],13)
 
 --
 
+Final model:
+
+find x: int(2..4)
+find y: int(2..4)
+find z: int(2..4)
+
+such that
+
+FlatWeightedSumLeq([2, 3, 1],[x, y, z],13)
+
diff --git a/conjure_oxide/tests/integration/basic/weighted-sum/02-simple-gt/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/weighted-sum/02-simple-gt/input-expected-rule-trace-human.txt
index 09687b6e77..116979e43b 100644
--- a/conjure_oxide/tests/integration/basic/weighted-sum/02-simple-gt/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/weighted-sum/02-simple-gt/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find x: int(2..4)
+find y: int(2..4)
+
+such that
+
+(Sum([Product([2, x]), Product([3, y])]) > 12)
+
+--
+
 (Sum([Product([2, x]), Product([3, y])]) > 12), 
    ~~> gt_to_geq ([("Minion", 8400)]) 
 (Sum([Sum([Product([2, x]), Product([3, y])]), -1]) >= 12) 
@@ -16,3 +27,12 @@ FlatWeightedSumGeq([2, 3, 1],[x, y, -1],12)
 
 --
 
+Final model:
+
+find x: int(2..4)
+find y: int(2..4)
+
+such that
+
+FlatWeightedSumGeq([2, 3, 1],[x, y, -1],12)
+
diff --git a/conjure_oxide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt
index 640a6f4bdf..3784b7b1fa 100644
--- a/conjure_oxide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find x: int(2..4)
+find y: int(2..4)
+
+such that
+
+(Sum([Product([2, x]), Product([3, y])]) = 12)
+
+--
+
 Sum([Product([2, x]), Product([3, y])]), 
    ~~> flatten_vecop ([("Minion", 4200)]) 
 Sum([__0, __1]) 
@@ -39,3 +50,16 @@ SumGeq([__0, __1], 12)
 
 --
 
+Final model:
+
+find x: int(2..4)
+find y: int(2..4)
+find __0: int(4..8)
+find __1: int(6..12)
+
+such that
+
+And([SumLeq([__0, __1], 12), SumGeq([__0, __1], 12)]),
+FlatProductEq(x,2,__0),
+FlatProductEq(y,3,__1)
+
diff --git a/conjure_oxide/tests/integration/basic/weighted-sum/04-needs-normalising/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/weighted-sum/04-needs-normalising/input-expected-rule-trace-human.txt
index 6931fa3e4a..47f653f69d 100644
--- a/conjure_oxide/tests/integration/basic/weighted-sum/04-needs-normalising/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/weighted-sum/04-needs-normalising/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(2..5)
+find y: int(2..5)
+find z: int(2..5)
+
+such that
+
+(Sum([Sum([Sum([Sum([Product([5, x]), Product([Product([Product([y, 3]), 1]), 3])]), -(Product([3, x]))]), Product([-(1), y])]), Product([y, -(5)])]) < 11)
+
+--
+
 -(1), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 -1 
@@ -76,3 +88,13 @@ FlatWeightedSumLeq([5, 9, -3, -1, -5],[x, y, x, y, y],10)
 
 --
 
+Final model:
+
+find x: int(2..5)
+find y: int(2..5)
+find z: int(2..5)
+
+such that
+
+FlatWeightedSumLeq([5, 9, -3, -1, -5],[x, y, x, y, y],10)
+
diff --git a/conjure_oxide/tests/integration/basic/weighted-sum/05-flattening/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/weighted-sum/05-flattening/input-expected-rule-trace-human.txt
index 7e72e1f276..524fc5087b 100644
--- a/conjure_oxide/tests/integration/basic/weighted-sum/05-flattening/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/weighted-sum/05-flattening/input-expected-rule-trace-human.txt
@@ -1,3 +1,20 @@
+Model before rewriting:
+
+find a: int(2..10)
+find b: int(2..10)
+find c: int(2..10)
+find d: int(2..10)
+find e: int(2..10)
+find f: int(2..10)
+find g: int(2..10)
+find h: int(2..10)
+
+such that
+
+(Sum([Sum([Sum([Sum([a, Product([2, b])]), Product([Product([3, c]), d])]), UnsafeDiv(e, f)]), Product([5, UnsafeDiv(g, h)])]) <= 18)
+
+--
+
 Sum([Sum([Sum([Sum([a, Product([2, b])]), Product([Product([3, c]), d])]), UnsafeDiv(e, f)]), Product([5, UnsafeDiv(g, h)])]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Sum([a, Product([2, b]), Product([Product([3, c]), d]), UnsafeDiv(e, f), Product([5, UnsafeDiv(g, h)])]) 
@@ -113,3 +130,24 @@ DivEq(g, h, __2)
 
 --
 
+Final model:
+
+find a: int(2..10)
+find b: int(2..10)
+find c: int(2..10)
+find d: int(2..10)
+find e: int(2..10)
+find f: int(2..10)
+find g: int(2..10)
+find h: int(2..10)
+find __0: int(4..100)
+find __1: int(0..5)
+find __2: int(0..5)
+
+such that
+
+And([FlatWeightedSumLeq([1, 2, 3, 1, 5],[a, b, __0, __1, __2],18), (h != 0), (f != 0)]),
+FlatProductEq(d,c,__0),
+DivEq(e, f, __1),
+DivEq(g, h, __2)
+
diff --git a/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input-expected-rule-trace-human.txt
index 535b7dee44..f3f8064a59 100644
--- a/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input-expected-rule-trace-human.txt
@@ -1,6 +1,24 @@
+Model before rewriting:
+
+find a: int(1..5)
+
+such that
+
+Or([])
+
+--
+
 Or([]), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 false 
 
 --
 
+Final model:
+
+find a: int(1..5)
+
+such that
+
+false
+
diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt
index f44f42ce43..304ce39d78 100644
--- a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find a: int(1..7)
+find b: int(1..7)
+
+such that
+
+(Sum([Min([a, b]), 6]) <= 10)
+
+--
+
 Min([a, b]), 
    ~~> min_to_var ([("Base", 6000)]) 
 __0 
@@ -27,3 +38,16 @@ Ineq(__0, b, 0)
 
 --
 
+Final model:
+
+find a: int(1..7)
+find b: int(1..7)
+find __0: int(1..7)
+
+such that
+
+SumLeq([__0, 6], 10),
+Ineq(__0, a, 0),
+Ineq(__0, b, 0),
+Or([(__0 = a), (__0 = b)])
+
diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input-expected-rule-trace-human.txt
index 9e11c7dabf..3c14037966 100644
--- a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input-expected-rule-trace-human.txt
@@ -1,3 +1,13 @@
+Model before rewriting:
+
+find c: int(1..7)
+
+such that
+
+(Sum([Min([5, 7]), c]) <= 10)
+
+--
+
 Min([5, 7]), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 5 
@@ -10,3 +20,11 @@ SumLeq([5, c], 10)
 
 --
 
+Final model:
+
+find c: int(1..7)
+
+such that
+
+SumLeq([5, c], 10)
+
diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input-expected-rule-trace-human.txt
index d9fe2e33fa..2e3a3112f2 100644
--- a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input-expected-rule-trace-human.txt
@@ -1,3 +1,19 @@
+Model before rewriting:
+
+find a: bool
+find b: bool
+find c: bool
+find d: bool
+
+such that
+
+Or([a, b]),
+Or([Not(c), And([b, d])]),
+b,
+Or([d, c])
+
+--
+
 Or([Not(c), And([b, d])]), 
    ~~> distribute_or_over_and ([("Base", 8400)]) 
 And([Or([Not(c), b]), Or([Not(c), d])]) 
@@ -16,3 +32,17 @@ WatchedLiteral(c,false)
 
 --
 
+Final model:
+
+find a: bool
+find b: bool
+find c: bool
+find d: bool
+
+such that
+
+Or([a, b]),
+And([Or([WatchedLiteral(c,false), b]), Or([WatchedLiteral(c,false), d])]),
+b,
+Or([d, c])
+
diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt
index 129f2c1ec0..b0b95e587b 100644
--- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find x: int(1..50)
+find y: int(1..50)
+
+such that
+
+(Sum([Sum([Sum([Sum([x, 10]), 20]), y]), 5]) = 100)
+
+--
+
 Sum([Sum([Sum([Sum([x, 10]), 20]), y]), 5]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Sum([x, 10, 20, y, 5]) 
@@ -28,3 +39,12 @@ SumGeq([x, y, 35], 100)
 
 --
 
+Final model:
+
+find x: int(1..50)
+find y: int(1..50)
+
+such that
+
+And([SumLeq([x, y, 35], 100), SumGeq([x, y, 35], 100)])
+
diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input-expected-rule-trace-human.txt
index e74f59cfab..0387a9b64a 100644
--- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input-expected-rule-trace-human.txt
@@ -1,3 +1,17 @@
+Model before rewriting:
+
+find a: bool
+find b: bool
+find c: bool
+
+such that
+
+Or([Or([a, b]), false]),
+Or([AllDiff([1, 2, 3]), true]),
+And([c, true])
+
+--
+
 Or([AllDiff([1, 2, 3]), true]), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 true 
@@ -28,3 +42,15 @@ c
 
 --
 
+Final model:
+
+find a: bool
+find b: bool
+find c: bool
+
+such that
+
+Or([a, b]),
+true,
+c
+
diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt
index 129f2c1ec0..b0b95e587b 100644
--- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find x: int(1..50)
+find y: int(1..50)
+
+such that
+
+(Sum([Sum([Sum([Sum([x, 10]), 20]), y]), 5]) = 100)
+
+--
+
 Sum([Sum([Sum([Sum([x, 10]), 20]), y]), 5]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Sum([x, 10, 20, y, 5]) 
@@ -28,3 +39,12 @@ SumGeq([x, y, 35], 100)
 
 --
 
+Final model:
+
+find x: int(1..50)
+find y: int(1..50)
+
+such that
+
+And([SumLeq([x, y, 35], 100), SumGeq([x, y, 35], 100)])
+
diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input-expected-rule-trace-human.txt
index e74f59cfab..0387a9b64a 100644
--- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input-expected-rule-trace-human.txt
@@ -1,3 +1,17 @@
+Model before rewriting:
+
+find a: bool
+find b: bool
+find c: bool
+
+such that
+
+Or([Or([a, b]), false]),
+Or([AllDiff([1, 2, 3]), true]),
+And([c, true])
+
+--
+
 Or([AllDiff([1, 2, 3]), true]), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 true 
@@ -28,3 +42,15 @@ c
 
 --
 
+Final model:
+
+find a: bool
+find b: bool
+find c: bool
+
+such that
+
+Or([a, b]),
+true,
+c
+
diff --git a/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt
index c88364b6e8..05ddb447dd 100644
--- a/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt
@@ -1,3 +1,16 @@
+Model before rewriting:
+
+find a: int(1..3)
+find b: int(1..3)
+find c: int(1..3)
+
+such that
+
+(Sum([Sum([a, b]), c]) = 4),
+(a >= b)
+
+--
+
 Sum([Sum([a, b]), c]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Sum([a, b, c]) 
@@ -28,3 +41,14 @@ Ineq(b, a, 0)
 
 --
 
+Final model:
+
+find a: int(1..3)
+find b: int(1..3)
+find c: int(1..3)
+
+such that
+
+And([SumLeq([a, b, c], 4), SumGeq([a, b, c], 4)]),
+Ineq(b, a, 0)
+
diff --git a/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt
index ec5615a43c..d2c0605c72 100644
--- a/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt
@@ -1,3 +1,16 @@
+Model before rewriting:
+
+find a: int(1..4)
+find b: int(1..4)
+find x: int(1..4)
+
+such that
+
+(Max([a, b]) >= 2),
+(x = Sum([Max([a, b]), 1]))
+
+--
+
 Max([a, b]), 
    ~~> max_to_var ([("Base", 6000)]) 
 __0 
@@ -68,3 +81,22 @@ Ineq(b, __1, 0)
 
 --
 
+Final model:
+
+find a: int(1..4)
+find b: int(1..4)
+find x: int(1..4)
+find __0: int(1..4)
+find __1: int(1..4)
+
+such that
+
+Ineq(2, __0, 0),
+And([SumLeq([__1, 1], x), Ineq(x, __1, 1)]),
+Ineq(a, __0, 0),
+Ineq(b, __0, 0),
+Or([(__0 = a), (__0 = b)]),
+Ineq(a, __1, 0),
+Ineq(b, __1, 0),
+Or([(__1 = a), (__1 = b)])
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/diseq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/diseq/input-expected-rule-trace-human.txt
index e69de29bb2..f9a326847b 100644
--- a/conjure_oxide/tests/integration/minion_constraints/diseq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/diseq/input-expected-rule-trace-human.txt
@@ -0,0 +1,20 @@
+Model before rewriting:
+
+find x: int(1..3)
+find y: int(1..3)
+
+such that
+
+(x != y)
+
+--
+
+Final model:
+
+find x: int(1..3)
+find y: int(1..3)
+
+such that
+
+(x != y)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-01-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-01-simple/input-expected-rule-trace-human.txt
index b1fb7b53b4..3401f339fe 100644
--- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-01-simple/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-01-simple/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find x: int(1..10)
+find y: int(2..4)
+
+such that
+
+(UnsafeDiv(x, y) = 5)
+
+--
+
 UnsafeDiv(x, y), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(x, y) @ (y != 0)} 
@@ -28,3 +39,12 @@ DivEq(x, y, 5)
 
 --
 
+Final model:
+
+find x: int(1..10)
+find y: int(2..4)
+
+such that
+
+And([DivEq(x, y, 5), (y != 0)])
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-02-zero/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-02-zero/input-expected-rule-trace-human.txt
index d0f4217606..46386a3a2e 100644
--- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-02-zero/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-02-zero/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(1..5)
+find y: int(0..2)
+find z: int(1..2)
+
+such that
+
+(UnsafeDiv(x, y) = z)
+
+--
+
 UnsafeDiv(x, y), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(x, y) @ (y != 0)} 
@@ -28,3 +40,13 @@ DivEq(x, y, z)
 
 --
 
+Final model:
+
+find x: int(1..5)
+find y: int(0..2)
+find z: int(1..2)
+
+such that
+
+And([DivEq(x, y, z), (y != 0)])
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt
index 159418c3a8..7735749dca 100644
--- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(5..20)
+find y: int(0..5)
+find z: int(0..6)
+
+such that
+
+(UnsafeDiv(x, UnsafeDiv(y, z)) = 10)
+
+--
+
 UnsafeDiv(y, z), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(y, z) @ (z != 0)} 
@@ -94,3 +106,17 @@ DivEq(y, z, __1)
 
 --
 
+Final model:
+
+find x: int(5..20)
+find y: int(0..5)
+find z: int(0..6)
+find __0: int(0..5)
+find __1: int(0..5)
+
+such that
+
+And([DivEq(x, __0, 10), (__1 != 0), (z != 0)]),
+DivEq(y, z, __0),
+DivEq(y, z, __1)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
index c3b64ff8e8..2aac0466cd 100644
--- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(5..20)
+find y: int(0..5)
+find z: int(0..6)
+
+such that
+
+(UnsafeDiv(x, UnsafeDiv(y, z)) != 10)
+
+--
+
 UnsafeDiv(y, z), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(y, z) @ (z != 0)} 
@@ -103,3 +115,19 @@ DivEq(y, z, __2)
 
 --
 
+Final model:
+
+find x: int(5..20)
+find y: int(0..5)
+find z: int(0..6)
+find __0: int(0..20)
+find __1: int(0..5)
+find __2: int(0..5)
+
+such that
+
+And([(__0 != 10), (__1 != 0), (z != 0)]),
+DivEq(x, __2, __0),
+DivEq(y, z, __1),
+DivEq(y, z, __2)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
index 45273a71da..1b8bbf1d1e 100644
--- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(5..20)
+find y: int(0..5)
+find z: int(0..6)
+
+such that
+
+Not((UnsafeDiv(x, UnsafeDiv(y, z)) = 10))
+
+--
+
 UnsafeDiv(y, z), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(y, z) @ (z != 0)} 
@@ -118,3 +130,17 @@ DivEq(y, z, __1)
 
 --
 
+Final model:
+
+find x: int(5..20)
+find y: int(0..5)
+find z: int(0..6)
+find __0: int(0..20)
+find __1: int(0..5)
+
+such that
+
+Or([(__0 != 10), DivEq(y, z, 0), (z = 0)]),
+DivEq(x, __1, __0),
+DivEq(y, z, __1)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/eq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/eq/input-expected-rule-trace-human.txt
index e69de29bb2..fa0841f050 100644
--- a/conjure_oxide/tests/integration/minion_constraints/eq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/eq/input-expected-rule-trace-human.txt
@@ -0,0 +1,20 @@
+Model before rewriting:
+
+find x: int(1..3)
+find y: int(1..2)
+
+such that
+
+(x = y)
+
+--
+
+Final model:
+
+find x: int(1..3)
+find y: int(1..2)
+
+such that
+
+(x = y)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/ineq-01-strict-less-than/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/ineq-01-strict-less-than/input-expected-rule-trace-human.txt
index a5a9deba29..e7bb6bcab9 100644
--- a/conjure_oxide/tests/integration/minion_constraints/ineq-01-strict-less-than/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/ineq-01-strict-less-than/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+(x < y)
+
+--
+
 (x < y), 
    ~~> lt_to_leq ([("Minion", 8400)]) 
 (x <= Sum([y, -1])) 
@@ -10,3 +21,12 @@ Ineq(x, y, -1)
 
 --
 
+Final model:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+Ineq(x, y, -1)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/ineq-02-leq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/ineq-02-leq/input-expected-rule-trace-human.txt
index 9b4c6def05..d9990f78fa 100644
--- a/conjure_oxide/tests/integration/minion_constraints/ineq-02-leq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/ineq-02-leq/input-expected-rule-trace-human.txt
@@ -1,6 +1,26 @@
+Model before rewriting:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+(x <= y)
+
+--
+
 (x <= y), 
    ~~> leq_to_ineq ([("Minion", 4100)]) 
 Ineq(x, y, 0) 
 
 --
 
+Final model:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+Ineq(x, y, 0)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/ineq-03-leq-plus-k/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/ineq-03-leq-plus-k/input-expected-rule-trace-human.txt
index 713306e4c1..db4faf1e80 100644
--- a/conjure_oxide/tests/integration/minion_constraints/ineq-03-leq-plus-k/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/ineq-03-leq-plus-k/input-expected-rule-trace-human.txt
@@ -1,6 +1,26 @@
+Model before rewriting:
+
+find x: int(1..3)
+find y: int(1..3)
+
+such that
+
+(x <= Sum([y, 2]))
+
+--
+
 (x <= Sum([y, 2])), 
    ~~> x_leq_y_plus_k_to_ineq ([("Minion", 4500)]) 
 Ineq(x, y, 2) 
 
 --
 
+Final model:
+
+find x: int(1..3)
+find y: int(1..3)
+
+such that
+
+Ineq(x, y, 2)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/ineq-04-strict-greater-than/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/ineq-04-strict-greater-than/input-expected-rule-trace-human.txt
index d9d4aa40ab..ba074fae55 100644
--- a/conjure_oxide/tests/integration/minion_constraints/ineq-04-strict-greater-than/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/ineq-04-strict-greater-than/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+(y > x)
+
+--
+
 (y > x), 
    ~~> gt_to_geq ([("Minion", 8400)]) 
 (Sum([y, -1]) >= x) 
@@ -10,3 +21,12 @@ Ineq(x, y, -1)
 
 --
 
+Final model:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+Ineq(x, y, -1)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/ineq-05-geq-plus-k-wrong-order/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/ineq-05-geq-plus-k-wrong-order/input-expected-rule-trace-human.txt
index 57a77e3f5b..8fe0957cf3 100644
--- a/conjure_oxide/tests/integration/minion_constraints/ineq-05-geq-plus-k-wrong-order/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/ineq-05-geq-plus-k-wrong-order/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+((y - 1) >= x),
+(Sum([-(1), y]) >= x)
+
+--
+
 -(1), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 -1 
@@ -28,3 +40,13 @@ Ineq(x, y, -1)
 
 --
 
+Final model:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+Ineq(x, y, -1),
+Ineq(x, y, -1)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/ineq-06-leq-plus-k-wrong-order/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/ineq-06-leq-plus-k-wrong-order/input-expected-rule-trace-human.txt
index 60d9822c91..f5e1dd9c31 100644
--- a/conjure_oxide/tests/integration/minion_constraints/ineq-06-leq-plus-k-wrong-order/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/ineq-06-leq-plus-k-wrong-order/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+(x <= (y - 1)),
+(x <= Sum([-(1), y]))
+
+--
+
 -(1), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 -1 
@@ -28,3 +40,13 @@ Ineq(x, y, -1)
 
 --
 
+Final model:
+
+find x: int(1..4)
+find y: int(1..4)
+
+such that
+
+Ineq(x, y, -1),
+Ineq(x, y, -1)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-01-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-01-simple/input-expected-rule-trace-human.txt
index 59ee5031d8..bdeb8c9f84 100644
--- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-01-simple/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-01-simple/input-expected-rule-trace-human.txt
@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find x: int(1..10)
+find y: int(2..4)
+
+such that
+
+(x % y = 3)
+
+--
+
 x % y, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(x,y) @ (y != 0)} 
@@ -28,3 +39,12 @@ ModEq(x, y, 3)
 
 --
 
+Final model:
+
+find x: int(1..10)
+find y: int(2..4)
+
+such that
+
+And([ModEq(x, y, 3), (y != 0)])
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-02-zero/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-02-zero/input-expected-rule-trace-human.txt
index 0f76195d77..2783460233 100644
--- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-02-zero/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-02-zero/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(1..5)
+find y: int(0..2)
+find z: int(1..2)
+
+such that
+
+(x % y = z)
+
+--
+
 x % y, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(x,y) @ (y != 0)} 
@@ -28,3 +40,13 @@ ModEq(x, y, z)
 
 --
 
+Final model:
+
+find x: int(1..5)
+find y: int(0..2)
+find z: int(1..2)
+
+such that
+
+And([ModEq(x, y, z), (y != 0)])
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt
index 0919ba0b8d..05b5a442a7 100644
--- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(5..20)
+find y: int(0..5)
+find z: int(0..6)
+
+such that
+
+(x % y % z = 3)
+
+--
+
 y % z, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(y,z) @ (z != 0)} 
@@ -94,3 +106,17 @@ ModEq(y, z, __1)
 
 --
 
+Final model:
+
+find x: int(5..20)
+find y: int(0..5)
+find z: int(0..6)
+find __0: int(0..5)
+find __1: int(0..5)
+
+such that
+
+And([ModEq(x, __0, 3), (__1 != 0), (z != 0)]),
+ModEq(y, z, __0),
+ModEq(y, z, __1)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
index 6131767942..dbdbcba0e3 100644
--- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(5..7)
+find y: int(0..3)
+find z: int(0..4)
+
+such that
+
+(x % y % z != 3)
+
+--
+
 y % z, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(y,z) @ (z != 0)} 
@@ -103,3 +115,19 @@ ModEq(y, z, __2)
 
 --
 
+Final model:
+
+find x: int(5..7)
+find y: int(0..3)
+find z: int(0..4)
+find __0: int(0..2)
+find __1: int(0..3)
+find __2: int(0..3)
+
+such that
+
+And([(__0 != 3), (__1 != 0), (z != 0)]),
+ModEq(x, __2, __0),
+ModEq(y, z, __1),
+ModEq(y, z, __2)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
index 1efa0e11dc..f18cba67c1 100644
--- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find x: int(5..7)
+find y: int(0..3)
+find z: int(0..4)
+
+such that
+
+Not((x % y % z = 3))
+
+--
+
 y % z, 
    ~~> mod_to_bubble ([("Bubble", 6000)]) 
 {SafeMod(y,z) @ (z != 0)} 
@@ -118,3 +130,17 @@ ModEq(y, z, __1)
 
 --
 
+Final model:
+
+find x: int(5..7)
+find y: int(0..3)
+find z: int(0..4)
+find __0: int(0..2)
+find __1: int(0..3)
+
+such that
+
+Or([(__0 != 3), ModEq(y, z, 0), (z = 0)]),
+ModEq(x, __1, __0),
+ModEq(y, z, __1)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/sumgeq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/sumgeq/input-expected-rule-trace-human.txt
index ab58bbf1cf..3235243736 100644
--- a/conjure_oxide/tests/integration/minion_constraints/sumgeq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/sumgeq/input-expected-rule-trace-human.txt
@@ -1,6 +1,28 @@
+Model before rewriting:
+
+find x: int(1..3)
+find y: int(1..3)
+find z: int(1..5)
+
+such that
+
+(Sum([x, y]) >= z)
+
+--
+
 (Sum([x, y]) >= z), 
    ~~> introduce_sumgeq ([("Minion", 4400)]) 
 SumGeq([x, y], z) 
 
 --
 
+Final model:
+
+find x: int(1..3)
+find y: int(1..3)
+find z: int(1..5)
+
+such that
+
+SumGeq([x, y], z)
+
diff --git a/conjure_oxide/tests/integration/minion_constraints/sumleq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/sumleq/input-expected-rule-trace-human.txt
index c00324929d..163eac5ab4 100644
--- a/conjure_oxide/tests/integration/minion_constraints/sumleq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/sumleq/input-expected-rule-trace-human.txt
@@ -1,6 +1,28 @@
+Model before rewriting:
+
+find x: int(1..3)
+find y: int(1..3)
+find z: int(1..5)
+
+such that
+
+(Sum([x, y]) <= z)
+
+--
+
 (Sum([x, y]) <= z), 
    ~~> introduce_sumleq ([("Minion", 4400)]) 
 SumLeq([x, y], z) 
 
 --
 
+Final model:
+
+find x: int(1..3)
+find y: int(1..3)
+find z: int(1..5)
+
+such that
+
+SumLeq([x, y], z)
+
diff --git a/conjure_oxide/tests/integration/savilerow/divide-mod-novar/divide-mod-novar-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/savilerow/divide-mod-novar/divide-mod-novar-expected-rule-trace-human.txt
index 75b4ebcfca..6e31571147 100644
--- a/conjure_oxide/tests/integration/savilerow/divide-mod-novar/divide-mod-novar-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/savilerow/divide-mod-novar/divide-mod-novar-expected-rule-trace-human.txt
@@ -1,3 +1,20 @@
+Model before rewriting:
+
+
+such that
+
+(UnsafeDiv(3, 2) = 1),
+(UnsafeDiv(-(3), 2) = -(2)),
+(UnsafeDiv(3, -(2)) = -(2)),
+(UnsafeDiv(-(3), -(2)) = 1),
+(3 % 2 = 1),
+(3 % -(2) = -(1)),
+(-(3) % 2 = 1),
+(-(3) % -(2) = -(1)),
+true
+
+--
+
 (UnsafeDiv(3, 2) = 1), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 true 
@@ -46,3 +63,18 @@ true
 
 --
 
+Final model:
+
+
+such that
+
+true,
+true,
+true,
+true,
+true,
+true,
+true,
+true,
+true
+
diff --git a/conjure_oxide/tests/integration/savilerow/divide-mod/divide-mod-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/savilerow/divide-mod/divide-mod-expected-rule-trace-human.txt
index 75b4ebcfca..98e0eb8bf1 100644
--- a/conjure_oxide/tests/integration/savilerow/divide-mod/divide-mod-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/savilerow/divide-mod/divide-mod-expected-rule-trace-human.txt
@@ -1,3 +1,21 @@
+Model before rewriting:
+
+find x: int(1..1)
+
+such that
+
+(UnsafeDiv(3, 2) = 1),
+(UnsafeDiv(-(3), 2) = -(2)),
+(UnsafeDiv(3, -(2)) = -(2)),
+(UnsafeDiv(-(3), -(2)) = 1),
+(3 % 2 = 1),
+(3 % -(2) = -(1)),
+(-(3) % 2 = 1),
+(-(3) % -(2) = -(1)),
+true
+
+--
+
 (UnsafeDiv(3, 2) = 1), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 true 
@@ -46,3 +64,19 @@ true
 
 --
 
+Final model:
+
+find x: int(1..1)
+
+such that
+
+true,
+true,
+true,
+true,
+true,
+true,
+true,
+true,
+true
+
diff --git a/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt
index c88364b6e8..05ddb447dd 100644
--- a/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt
@@ -1,3 +1,16 @@
+Model before rewriting:
+
+find a: int(1..3)
+find b: int(1..3)
+find c: int(1..3)
+
+such that
+
+(Sum([Sum([a, b]), c]) = 4),
+(a >= b)
+
+--
+
 Sum([Sum([a, b]), c]), 
    ~~> normalise_associative_commutative ([("Base", 8900)]) 
 Sum([a, b, c]) 
@@ -28,3 +41,14 @@ Ineq(b, a, 0)
 
 --
 
+Final model:
+
+find a: int(1..3)
+find b: int(1..3)
+find c: int(1..3)
+
+such that
+
+And([SumLeq([a, b, c], 4), SumGeq([a, b, c], 4)]),
+Ineq(b, a, 0)
+
diff --git a/conjure_oxide/tests/model_tests.rs b/conjure_oxide/tests/model_tests.rs
index 39d749d1db..ef1efb536e 100644
--- a/conjure_oxide/tests/model_tests.rs
+++ b/conjure_oxide/tests/model_tests.rs
@@ -1,6 +1,6 @@
 // Tests for various functionalities of the Model
 
-use std::collections::HashMap;
+use std::collections::BTreeMap;
 
 use conjure_core::model::Model;
 use conjure_oxide::ast::*;
@@ -12,7 +12,7 @@ fn modify_domain() {
     let d1 = Domain::IntDomain(vec![Range::Bounded(1, 3)]);
     let d2 = Domain::IntDomain(vec![Range::Bounded(1, 2)]);
 
-    let mut variables = HashMap::new();
+    let mut variables = BTreeMap::new();
     variables.insert(a.clone(), DecisionVariable { domain: d1.clone() });
 
     let mut m = Model::new(variables, vec![], Default::default());
diff --git a/conjure_oxide/tests/rewrite_tests.rs b/conjure_oxide/tests/rewrite_tests.rs
index b0e325afcd..7162081451 100644
--- a/conjure_oxide/tests/rewrite_tests.rs
+++ b/conjure_oxide/tests/rewrite_tests.rs
@@ -1,4 +1,4 @@
-use std::collections::HashMap;
+use std::collections::BTreeMap;
 use std::process::exit;
 
 use conjure_core::rules::eval_constant;
@@ -320,7 +320,7 @@ fn reduce_solve_xyz() {
         )
     );
 
-    let mut model = Model::new(HashMap::new(), vec![expr1, expr2], Default::default());
+    let mut model = Model::new(BTreeMap::new(), vec![expr1, expr2], Default::default());
     model.variables.insert(
         Name::UserName(String::from("a")),
         DecisionVariable {
@@ -656,7 +656,7 @@ fn rewrite_solve_xyz() {
 
     // Apply rewrite function to the nested expression
     let rewritten_expr = rewrite_model(
-        &Model::new(HashMap::new(), vec![nested_expr], Default::default()),
+        &Model::new(BTreeMap::new(), vec![nested_expr], Default::default()),
         &rule_sets,
     )
     .unwrap()
@@ -667,7 +667,7 @@ fn rewrite_solve_xyz() {
     assert!(rewritten_expr.iter().all(is_simple));
 
     // Create model with variables and constraints
-    let mut model = Model::new(HashMap::new(), rewritten_expr, Default::default());
+    let mut model = Model::new(BTreeMap::new(), rewritten_expr, Default::default());
 
     // Insert variables and domains
     model.variables.insert(
diff --git a/crates/conjure_core/src/ast/symbol_table.rs b/crates/conjure_core/src/ast/symbol_table.rs
index 0e7fef0a74..aa9165e204 100644
--- a/crates/conjure_core/src/ast/symbol_table.rs
+++ b/crates/conjure_core/src/ast/symbol_table.rs
@@ -1,4 +1,4 @@
-use std::collections::HashMap;
+use std::collections::BTreeMap;
 use std::fmt::Display;
 
 use serde::{Deserialize, Serialize};
@@ -23,4 +23,4 @@ impl Display for Name {
     }
 }
 
-pub type SymbolTable = HashMap<Name, DecisionVariable>;
+pub type SymbolTable = BTreeMap<Name, DecisionVariable>;
diff --git a/crates/conjure_core/src/model.rs b/crates/conjure_core/src/model.rs
index 4e03e8f065..46b6c46f78 100644
--- a/crates/conjure_core/src/model.rs
+++ b/crates/conjure_core/src/model.rs
@@ -1,6 +1,6 @@
 use std::cell::RefCell;
 use std::collections::HashSet;
-use std::fmt::Debug;
+use std::fmt::{Debug, Display};
 use std::sync::{Arc, RwLock};
 
 use derivative::Derivative;
@@ -10,6 +10,8 @@ use serde_with::serde_as;
 use crate::ast::{DecisionVariable, Domain, Expression, Name, SymbolTable};
 use crate::context::Context;
 
+use crate::ast::pretty::{pretty_expressions_as_top_level, pretty_variable_declaration};
+
 /// Represents a computational model containing variables, constraints, and a shared context.
 ///
 /// The `Model` struct holds a set of variables and constraints for manipulating and evaluating symbolic expressions.
@@ -146,3 +148,22 @@ impl Model {
         self.variables.extend(symbol_table);
     }
 }
+
+impl Display for Model {
+    #[allow(clippy::unwrap_used)] // [rustdocs]: should only fail iff the formatter fails
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        for name in self.variables.keys() {
+            writeln!(
+                f,
+                "find {}",
+                pretty_variable_declaration(&self.variables, name).unwrap()
+            )?;
+        }
+
+        writeln!(f, "\nsuch that\n")?;
+
+        writeln!(f, "{}", pretty_expressions_as_top_level(&self.constraints))?;
+
+        Ok(())
+    }
+}
diff --git a/crates/conjure_core/src/parse/example_models.rs b/crates/conjure_core/src/parse/example_models.rs
index fc0f6ef926..d99a7b3652 100644
--- a/crates/conjure_core/src/parse/example_models.rs
+++ b/crates/conjure_core/src/parse/example_models.rs
@@ -29,7 +29,7 @@ pub fn get_example_model(filename: &str) -> Result<Model, anyhow::Error> {
         if path.is_file()
             && path
                 .extension()
-                .map_or(false, |e| e == "essence" || e == "eprime")
+                .is_some_and(|e| e == "essence" || e == "eprime")
             && path.file_stem() == Some(std::ffi::OsStr::new(filename))
         {
             essence_path = path.to_path_buf();
diff --git a/crates/conjure_core/src/solver/adaptors/minion/adaptor.rs b/crates/conjure_core/src/solver/adaptors/minion/adaptor.rs
index d39c1d9320..b696c2b3de 100644
--- a/crates/conjure_core/src/solver/adaptors/minion/adaptor.rs
+++ b/crates/conjure_core/src/solver/adaptors/minion/adaptor.rs
@@ -48,6 +48,7 @@ fn minion_rs_callback(solutions: HashMap<minion_ast::VarName, minion_ast::Consta
         .unwrap();
 
     let mut conjure_solutions: HashMap<conjure_ast::Name, conjure_ast::Literal> = HashMap::new();
+    let machine_name_re = Regex::new(r"__conjure_machine_name_([0-9]+)").unwrap();
     for (minion_name, minion_const) in solutions.into_iter() {
         let conjure_const = match minion_const {
             minion_ast::Constant::Bool(x) => conjure_ast::Literal::Bool(x),
@@ -55,7 +56,6 @@ fn minion_rs_callback(solutions: HashMap<minion_ast::VarName, minion_ast::Consta
             _ => todo!(),
         };
 
-        let machine_name_re = Regex::new(r"__conjure_machine_name_([0-9]+)").unwrap();
         let conjure_name = if let Some(caps) = machine_name_re.captures(&minion_name) {
             conjure_ast::Name::MachineName(caps[1].parse::<i32>().unwrap())
         } else {