diff --git a/CHANGELOG.md b/CHANGELOG.md
index af7df6541..7a4830867 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 ### Changed
+
+- Improved performance of small frequently allocated values (#1761)
+
 ### Deprecated
 ### Removed
 ### Fixed
diff --git a/evaluator/src/builtins.rs b/evaluator/src/builtins.rs
index fd3edaeb3..904f231df 100644
--- a/evaluator/src/builtins.rs
+++ b/evaluator/src/builtins.rs
@@ -24,7 +24,6 @@ use crate::ir::QuintError;
 use crate::value::{ImmutableMap, ImmutableSet, ImmutableVec, Value};
 use fxhash::FxHashSet;
 use itertools::Itertools;
-use std::rc::Rc;
 
 /// A list of operators that need to be compiled lazily (with `compile_lazy_op`).
 pub const LAZY_OPS: [&str; 13] = [
@@ -52,26 +51,26 @@ pub fn compile_lazy_op(op: &str) -> CompiledExprWithLazyArgs {
             for arg in args {
                 let result = arg.execute(env)?;
                 if !result.as_bool() {
-                    return Ok(Value::Bool(false));
+                    return Ok(Value::bool(false));
                 }
             }
-            Ok(Value::Bool(true))
+            Ok(Value::bool(true))
         },
         "or" => |env, args| {
             // Short-circuit logical OR
             for arg in args {
                 let result = arg.execute(env)?;
                 if result.as_bool() {
-                    return Ok(Value::Bool(true));
+                    return Ok(Value::bool(true));
                 }
             }
-            Ok(Value::Bool(false))
+            Ok(Value::bool(false))
         },
         "implies" => |env, args| {
             // Short-circuit logical implication
             let lhs = args[0].execute(env)?;
             if !lhs.as_bool() {
-                return Ok(Value::Bool(true));
+                return Ok(Value::bool(true));
             }
 
             args[1].execute(env)
@@ -96,13 +95,13 @@ pub fn compile_lazy_op(op: &str) -> CompiledExprWithLazyArgs {
                 if result.as_bool() {
                     // Found an enabled action - record it and return true
                     // TODO: Record in the trace recorder
-                    return Ok(Value::Bool(true));
+                    return Ok(Value::bool(true));
                 }
 
                 // Reset state before trying next action
                 env.var_storage.borrow_mut().restore(&next_vars_snapshot);
             }
-            Ok(Value::Bool(false))
+            Ok(Value::bool(false))
         },
         "actionAll" => |env, args| {
             // Executes all of the given actions, or none of them if any of them results in false.
@@ -112,10 +111,10 @@ pub fn compile_lazy_op(op: &str) -> CompiledExprWithLazyArgs {
                 let result = action.execute(env)?;
                 if !result.as_bool() {
                     env.var_storage.borrow_mut().restore(&next_vars_snapshot);
-                    return Ok(Value::Bool(false));
+                    return Ok(Value::bool(false));
                 }
             }
-            Ok(Value::Bool(true))
+            Ok(Value::bool(true))
         },
         "ite" => |env, args| {
             // if-then-else
@@ -202,10 +201,10 @@ pub fn compile_lazy_op(op: &str) -> CompiledExprWithLazyArgs {
                 // Repeats the given action n times, stopping if the action evaluates to false.
                 let reps = args[0].execute(env).map(|r| r.as_int())?;
                 let action = &args[1];
-                let mut result = Value::Bool(true);
+                let mut result = Value::bool(true);
                 for i in 0..reps {
                     let closure = action.execute(env)?;
-                    result = closure.as_closure()(env, vec![Value::Int(i)])?;
+                    result = closure.as_closure()(env, vec![Value::int(i)])?;
                     if !result.as_bool() {
                         return Err(QuintError::new(
                             "QNT513",
@@ -251,7 +250,7 @@ pub fn compile_lazy_op(op: &str) -> CompiledExprWithLazyArgs {
                     ));
                 }
 
-                Ok(Value::Bool(true))
+                Ok(Value::bool(true))
             }
         }
         _ => {
@@ -273,41 +272,41 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
 
     CompiledExprWithArgs::from_fn(match op {
         // Constructs a set from the given arguments.
-        "Set" => |_env, args| Ok(Value::Set(args.into_iter().collect())),
+        "Set" => |_env, args| Ok(Value::set(args.into_iter().collect())),
         "Rec" => |_env, args| {
             // Constructs a record from the given arguments. Arguments are lists like [key1, value1, key2, value2, ...]
-            Ok(Value::Record(
+            Ok(Value::record(
                 args.chunks_exact(2)
                     .map(|chunk| (chunk[0].as_str(), chunk[1].clone()))
                     .collect(),
             ))
         },
         // Constructs a tuple from the given arguments.
-        "Tup" => |_env, args| Ok(Value::Tuple(args.into_iter().collect())),
+        "Tup" => |_env, args| Ok(Value::tuple(args.into_iter().collect())),
         // Constructs a list from the given arguments.
-        "List" => |_env, args| Ok(Value::List(args.into_iter().collect())),
+        "List" => |_env, args| Ok(Value::list(args.into_iter().collect())),
         // Constructs a map from the given arguments. Arguments are lists like [[key1, value1], [key2, value2], ...]
         "Map" => |_env, args| {
-            Ok(Value::Map(
+            Ok(Value::map(
                 args.into_iter().map(|kv| kv.as_tuple2()).collect(),
             ))
         },
         // Constructs a variant from the given arguments.
-        "variant" => |_env, args| Ok(Value::Variant(args[0].as_str(), Rc::new(args[1].clone()))),
+        "variant" => |_env, args| Ok(Value::variant(args[0].as_str(), args[1].clone())),
         // Logical negation
-        "not" => |_env, args| Ok(Value::Bool(!args[0].as_bool())),
+        "not" => |_env, args| Ok(Value::bool(!args[0].as_bool())),
         // Logical equivalence/bi-implication
-        "iff" => |_env, args| Ok(Value::Bool(args[0].as_bool() == args[1].as_bool())),
+        "iff" => |_env, args| Ok(Value::bool(args[0].as_bool() == args[1].as_bool())),
         // Equality
-        "eq" => |_env, args| Ok(Value::Bool(args[0] == args[1])),
+        "eq" => |_env, args| Ok(Value::bool(args[0] == args[1])),
         // Inequality
-        "neq" => |_env, args| Ok(Value::Bool(args[0] != args[1])),
+        "neq" => |_env, args| Ok(Value::bool(args[0] != args[1])),
         // Integer addition
-        "iadd" => |_env, args| Ok(Value::Int(args[0].as_int() + args[1].as_int())),
+        "iadd" => |_env, args| Ok(Value::int(args[0].as_int() + args[1].as_int())),
         // Integer subtraction
-        "isub" => |_env, args| Ok(Value::Int(args[0].as_int() - args[1].as_int())),
+        "isub" => |_env, args| Ok(Value::int(args[0].as_int() - args[1].as_int())),
         // Integer multiplication
-        "imul" => |_env, args| Ok(Value::Int(args[0].as_int() * args[1].as_int())),
+        "imul" => |_env, args| Ok(Value::int(args[0].as_int() * args[1].as_int())),
         // Integer division
         "idiv" => |_env, args| {
             let divisor = args[1].as_int();
@@ -315,10 +314,10 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
                 return Err(QuintError::new("QNT503", "Division by zero"));
             }
 
-            Ok(Value::Int(args[0].as_int() / divisor))
+            Ok(Value::int(args[0].as_int() / divisor))
         },
         // Integer modulus
-        "imod" => |_env, args| Ok(Value::Int(args[0].as_int() % args[1].as_int())),
+        "imod" => |_env, args| Ok(Value::int(args[0].as_int() % args[1].as_int())),
         // Integer exponentiation
         "ipow" => |_env, args| {
             let base = args[0].as_int();
@@ -330,29 +329,29 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
                 return Err(QuintError::new("QNT503", "i^j is undefined for j < 0"));
             }
 
-            Ok(Value::Int(base.pow(exp as u32)))
+            Ok(Value::int(base.pow(exp as u32)))
         },
         // Integer unary minus
-        "iuminus" => |_env, args| Ok(Value::Int(-args[0].as_int())),
+        "iuminus" => |_env, args| Ok(Value::int(-args[0].as_int())),
         // Integer less than
-        "ilt" => |_env, args| Ok(Value::Bool(args[0].as_int() < args[1].as_int())),
+        "ilt" => |_env, args| Ok(Value::bool(args[0].as_int() < args[1].as_int())),
         // Integer less than or equal to
-        "ilte" => |_env, args| Ok(Value::Bool(args[0].as_int() <= args[1].as_int())),
+        "ilte" => |_env, args| Ok(Value::bool(args[0].as_int() <= args[1].as_int())),
         // Integer greater than
-        "igt" => |_env, args| Ok(Value::Bool(args[0].as_int() > args[1].as_int())),
+        "igt" => |_env, args| Ok(Value::bool(args[0].as_int() > args[1].as_int())),
         // Integer greater than or equal to
-        "igte" => |_env, args| Ok(Value::Bool(args[0].as_int() >= args[1].as_int())),
+        "igte" => |_env, args| Ok(Value::bool(args[0].as_int() >= args[1].as_int())),
 
         // Access a tuple: tuples are 1-indexed, that is, _1, _2, etc.
         "item" => |_env, args| at_index(args[0].as_list(), args[1].as_int() - 1),
         // A set of all possible tuples from the elements of the respective given sets.
-        "tuples" => |_env, args| Ok(Value::CrossProduct(args)),
+        "tuples" => |_env, args| Ok(Value::cross_product(args)),
 
         // Constructs a list of integers from start to end.
         "range" => |_env, args| {
             let start = args[0].as_int();
             let end = args[1].as_int();
-            Ok(Value::List((start..end).map(Value::Int).collect()))
+            Ok(Value::list((start..end).map(Value::int).collect()))
         },
         // List access
         "nth" => |_env, args| at_index(args[0].as_list(), args[1].as_int()),
@@ -369,7 +368,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
             }
 
             list[index as usize] = args[2].clone();
-            Ok(Value::List(list))
+            Ok(Value::list(list))
         },
 
         // Get the first element of a list. Not allowed in empty lists.
@@ -385,7 +384,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
         "tail" => |_env, args| {
             let list = args[0].as_list();
             if !list.is_empty() {
-                Ok(Value::List(list.iter().skip(1).cloned().collect()))
+                Ok(Value::list(list.iter().skip(1).cloned().collect()))
             } else {
                 Err(QuintError::new("QNT505", "Called 'tail' on an empty list"))
             }
@@ -398,7 +397,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
             let end = args[2].as_int() as usize;
 
             if start >= 0 && end <= list.len() && start as usize <= end {
-                Ok(Value::List(list.clone().slice(start as usize..end)))
+                Ok(Value::list(list.clone().slice(start as usize..end)))
             } else {
                 Err(QuintError::new(
                     "QNT506",
@@ -414,23 +413,23 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
         },
 
         // The length of a list.
-        "length" => |_env, args| Ok(Value::Int(args[0].cardinality().try_into().unwrap())),
+        "length" => |_env, args| Ok(Value::int(args[0].cardinality().try_into().unwrap())),
         // Append an element to a list.
         "append" => |_env, args| {
             let mut list = args[0].as_list().clone();
             list.push_back(args[1].clone());
-            Ok(Value::List(list))
+            Ok(Value::list(list))
         },
         // Concatenate two lists.
         "concat" => |_env, args| {
             let mut list = args[0].as_list().clone();
             list.extend(args[1].as_list().iter().cloned());
-            Ok(Value::List(list))
+            Ok(Value::list(list))
         },
         // A set with the indices of a list.
         "indices" => |_env, args| {
             let size: i64 = args[0].cardinality().try_into().unwrap();
-            Ok(Value::Interval(0, size - 1))
+            Ok(Value::interval(0, size - 1))
         },
 
         // Access a field in a record.
@@ -444,11 +443,11 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
 
         // A set with the field names of a record.
         "fieldNames" => |_env, args| {
-            Ok(Value::Set(
+            Ok(Value::set(
                 args[0]
                     .as_record_map()
                     .keys()
-                    .map(|s| Value::Str(s.clone()))
+                    .map(|s| Value::str(s.clone()))
                     .collect(),
             ))
         },
@@ -457,20 +456,20 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
         "with" => |_env, args| {
             let mut record = args[0].as_record_map().clone();
             record.insert(args[1].as_str(), args[2].clone());
-            Ok(Value::Record(record))
+            Ok(Value::record(record))
         },
 
         // The powerset of a set.
-        "powerset" => |_env, args| Ok(Value::PowerSet(Rc::new(args[0].clone()))),
+        "powerset" => |_env, args| Ok(Value::power_set(args[0].clone())),
         // Check if a set contains an element.
-        "contains" => |_env, args| Ok(Value::Bool(args[0].contains(&args[1]))),
+        "contains" => |_env, args| Ok(Value::bool(args[0].contains(&args[1]))),
         // Check if an element is in a set.
-        "in" => |_env, args| Ok(Value::Bool(args[1].contains(&args[0]))),
+        "in" => |_env, args| Ok(Value::bool(args[1].contains(&args[0]))),
         // Check if a set is a subset of another set.
-        "subseteq" => |_env, args| Ok(Value::Bool(args[0].subseteq(&args[1]))),
+        "subseteq" => |_env, args| Ok(Value::bool(args[0].subseteq(&args[1]))),
         // Set difference.
         "exclude" => |_env, args| {
-            Ok(Value::Set(
+            Ok(Value::set(
                 args[0]
                     .as_set()
                     .into_owned()
@@ -479,7 +478,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
         },
         // Set union.
         "union" => |_env, args| {
-            Ok(Value::Set(
+            Ok(Value::set(
                 args[0]
                     .as_set()
                     .into_owned()
@@ -488,7 +487,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
         },
         // Set intersection.
         "intersect" => |_env, args| {
-            Ok(Value::Set(
+            Ok(Value::set(
                 args[0]
                     .as_set()
                     .into_owned()
@@ -497,12 +496,12 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
         },
 
         // The size of a set.
-        "size" => |_env, args| Ok(Value::Int(args[0].cardinality().try_into().unwrap())),
+        "size" => |_env, args| Ok(Value::int(args[0].cardinality().try_into().unwrap())),
 
         // Whether a set is finite.
         "isFinite" => |_env, _args| {
             // at the moment, we support only finite sets, so just return true
-            Ok(Value::Bool(true))
+            Ok(Value::bool(true))
         },
         // Construct a set of integers from a to b.
         "to" => |_env, args| {
@@ -510,9 +509,9 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
             let end = args[1].as_int();
             if start > end {
                 // Avoid having different intervals that represent the same thing (empty set)
-                return Ok(Value::Set(ImmutableSet::default()));
+                return Ok(Value::set(ImmutableSet::default()));
             }
-            Ok(Value::Interval(start, end))
+            Ok(Value::interval(start, end))
         },
 
         // Fold a set
@@ -547,7 +546,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
 
         // Flatten a set of sets.
         "flatten" => |_env, args| {
-            Ok(Value::Set(
+            Ok(Value::set(
                 args[0]
                     .as_set()
                     .iter()
@@ -587,7 +586,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
             }
 
             map.insert(key, args[2].clone());
-            Ok(Value::Map(map))
+            Ok(Value::map(map))
         },
 
         // Set a value for any key in a map.
@@ -596,7 +595,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
             let key = args[1].clone().normalize();
             let value = args[2].clone();
             map.insert(key, value);
-            Ok(Value::Map(map))
+            Ok(Value::map(map))
         },
 
         // Set a value for an existing key in a map using a lambda over the current value.
@@ -607,7 +606,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
                 Some(value) => {
                     let new_value = args[2].as_closure()(env, vec![value.clone()])?;
                     map.insert(key, new_value);
-                    Ok(Value::Map(map))
+                    Ok(Value::map(map))
                 }
                 None => Err(QuintError::new(
                     "QNT507",
@@ -617,45 +616,47 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
         },
 
         // A set with the keys of a map.
-        "keys" => |_env, args| Ok(Value::Set(args[0].as_map().keys().cloned().collect())),
+        "keys" => |_env, args| Ok(Value::set(args[0].as_map().keys().cloned().collect())),
         // Check if a predicate holds for some element in a set.
         "exists" => |env, args| {
+            let c = args[1].as_closure();
             for v in args[0].as_set().iter() {
-                let result = args[1].as_closure()(env, vec![v.clone()])?;
-                if result.as_bool() {
-                    return Ok(Value::Bool(true));
+                if c(env, vec![v.clone()])?.as_bool() {
+                    return Ok(Value::bool(true));
                 }
             }
-            Ok(Value::Bool(false))
+            Ok(Value::bool(false))
         },
 
         "forall" => |env, args| {
+            let c = args[1].as_closure();
             for v in args[0].as_set().iter() {
-                let result = args[1].as_closure()(env, vec![v.clone()])?;
-                if !result.as_bool() {
-                    return Ok(Value::Bool(false));
+                if !c(env, vec![v.clone()])?.as_bool() {
+                    return Ok(Value::bool(false));
                 }
             }
-            Ok(Value::Bool(true))
+            Ok(Value::bool(true))
         },
 
         // Map a lambda over a set.
         "map" => |env, args| {
-            Ok(Value::Set(
+            let c = args[1].as_closure();
+            Ok(Value::set(
                 args[0]
                     .as_set()
                     .iter()
-                    .map(|v| args[1].as_closure()(env, vec![v.clone()]))
+                    .map(|v| c(env, vec![v.clone()]))
                     .collect::<Result<_, _>>()?,
             ))
         },
 
         // Filter a set using a lambda.
         "filter" => |env, args| {
-            Ok(Value::Set(args[0].as_set().iter().try_fold(
+            let c = args[1].as_closure();
+            Ok(Value::set(args[0].as_set().iter().try_fold(
                 ImmutableSet::default(),
                 |mut acc, v| {
-                    if args[1].as_closure()(env, vec![v.clone()])?.as_bool() {
+                    if c(env, vec![v.clone()])?.as_bool() {
                         acc.insert(v.clone());
                     }
                     Ok(acc)
@@ -665,10 +666,11 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
 
         // Filter a list using a lambda
         "select" => |env, args| {
-            Ok(Value::List(args[0].as_list().iter().try_fold(
+            let c = args[1].as_closure();
+            Ok(Value::list(args[0].as_list().iter().try_fold(
                 ImmutableVec::new(),
                 |mut acc, v| {
-                    if args[1].as_closure()(env, vec![v.clone()])?.as_bool() {
+                    if c(env, vec![v.clone()])?.as_bool() {
                         acc.push_back(v.clone());
                     }
                     Ok(acc)
@@ -681,7 +683,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
             let closure = args[1].as_closure();
             let keys = args[0].as_set();
 
-            Ok(Value::Map(keys.iter().try_fold(
+            Ok(Value::map(keys.iter().try_fold(
                 ImmutableMap::new(),
                 |mut acc, key| {
                     let value = closure(env, vec![key.clone()])?;
@@ -693,23 +695,18 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
         // Convert a set of key-value tuples to a map.
         "setToMap" => |_env, args| {
             let set = args[0].as_set();
-            Ok(Value::Map(set.iter().map(|v| v.as_tuple2()).collect()))
+            Ok(Value::map(set.iter().map(|v| v.as_tuple2()).collect()))
         },
         // A set of all possible maps with keys and values from the given sets.
-        "setOfMaps" => |_env, args| {
-            Ok(Value::MapSet(
-                Rc::new(args[0].clone()),
-                Rc::new(args[1].clone()),
-            ))
-        },
+        "setOfMaps" => |_env, args| Ok(Value::map_set(args[0].clone(), args[1].clone())),
         // Expect a value to be false
-        "fail" => |_env, args| Ok(Value::Bool(!args[0].as_bool())),
+        "fail" => |_env, args| Ok(Value::bool(!args[0].as_bool())),
         // Expect a value to be true, returning a runtime error if it is not
         "assert" => |_env, args| {
             if !args[0].as_bool() {
                 return Err(QuintError::new("QNT508", "Assertion failed"));
             }
-            Ok(Value::Bool(true))
+            Ok(Value::bool(true))
         },
         // Generate all lists of length up to the given number, from a set
         "allListsUpTo" => |_env, args| {
@@ -734,7 +731,7 @@ pub fn compile_eager_op(op: &str) -> CompiledExprWithArgs {
                 last_lists = new_lists;
             }
 
-            Ok(Value::Set(lists.into_iter().map(Value::List).collect()))
+            Ok(Value::set(lists.into_iter().map(Value::list).collect()))
         },
 
         // Get the only element of a set, or an error if the set is empty or has more than one element.
@@ -820,23 +817,23 @@ mod tests {
     // [3,2,1]
     #[test]
     fn test_fold_left() {
-        let list = vec![Value::Int(1), Value::Int(2), Value::Int(3)];
+        let list = vec![Value::int(1), Value::int(2), Value::int(3)];
         let result = fold_left(
             list.into_iter(),
-            Value::List(ImmutableVec::new()),
+            Value::list(ImmutableVec::new()),
             |acc, arg| {
                 let mut acc = acc.as_list().clone();
                 acc.push_front(arg);
-                Ok(Value::List(acc))
+                Ok(Value::list(acc))
             },
         );
 
         assert_eq!(
             result.unwrap(),
-            Value::List(ImmutableVec::from(vec![
-                Value::Int(3),
-                Value::Int(2),
-                Value::Int(1),
+            Value::list(ImmutableVec::from(vec![
+                Value::int(3),
+                Value::int(2),
+                Value::int(1),
             ]))
         );
     }
@@ -845,23 +842,23 @@ mod tests {
     // [1,2,3]
     #[test]
     fn test_fold_right() {
-        let list = vec![Value::Int(1), Value::Int(2), Value::Int(3)];
+        let list = vec![Value::int(1), Value::int(2), Value::int(3)];
         let result = fold_right(
             list.into_iter(),
-            Value::List(ImmutableVec::new()),
+            Value::list(ImmutableVec::new()),
             |arg, acc| {
                 let mut acc = acc.as_list().clone();
                 acc.push_front(arg);
-                Ok(Value::List(acc))
+                Ok(Value::list(acc))
             },
         );
 
         assert_eq!(
             result.unwrap(),
-            Value::List(ImmutableVec::from(vec![
-                Value::Int(1),
-                Value::Int(2),
-                Value::Int(3)
+            Value::list(ImmutableVec::from(vec![
+                Value::int(1),
+                Value::int(2),
+                Value::int(3)
             ]))
         );
     }
diff --git a/evaluator/src/evaluator.rs b/evaluator/src/evaluator.rs
index 3e73dfa8e..035cd1489 100644
--- a/evaluator/src/evaluator.rs
+++ b/evaluator/src/evaluator.rs
@@ -441,7 +441,7 @@ impl<'a> Interpreter<'a> {
             })
             .collect::<Vec<_>>();
 
-        Value::Lambda(registers, body)
+        Value::lambda(registers, body)
     }
 
     pub fn compile(&mut self, expr: &QuintEx) -> CompiledExpr {
@@ -470,17 +470,17 @@ impl<'a> Interpreter<'a> {
         match expr {
             QuintEx::QuintInt { id: _, value } => {
                 let value = *value;
-                CompiledExpr::new(move |_| Ok(Value::Int(value)))
+                CompiledExpr::new(move |_| Ok(Value::int(value)))
             }
 
             QuintEx::QuintBool { id: _, value } => {
                 let value = *value;
-                CompiledExpr::new(move |_| Ok(Value::Bool(value)))
+                CompiledExpr::new(move |_| Ok(Value::bool(value)))
             }
 
             QuintEx::QuintStr { id: _, value } => {
                 let value = value.clone();
-                CompiledExpr::new(move |_| Ok(Value::Str(value.clone())))
+                CompiledExpr::new(move |_| Ok(Value::str(value.clone())))
             }
 
             QuintEx::QuintName { id, name } => self
@@ -515,7 +515,7 @@ impl<'a> Interpreter<'a> {
                         CompiledExpr::new(move |env| {
                             let value = expr.execute(env)?;
                             register.borrow_mut().value = Some(value.clone());
-                            Ok(Value::Bool(true))
+                            Ok(Value::bool(true))
                         })
                     })
                 } else if LAZY_OPS.contains(&opcode.as_str()) {
@@ -546,7 +546,6 @@ impl<'a> Interpreter<'a> {
                     // Check if this is specifically a oneOf application
                     if let QuintEx::QuintApp { opcode, args, .. } = &opdef.expr {
                         if opcode == "oneOf" && args.len() == 1 {
-                            // Special handling for nondet oneOf on potentially empty sets
                             let set_expr = self.compile(&args[0]);
                             let cached_value = {
                                 let cached = self
@@ -607,12 +606,12 @@ impl<'a> Interpreter<'a> {
 
 fn builtin_value(name: &str) -> CompiledExpr {
     match name {
-        "true" => CompiledExpr::new(move |_| Ok(Value::Bool(true))),
-        "false" => CompiledExpr::new(move |_| Ok(Value::Bool(false))),
+        "true" => CompiledExpr::new(move |_| Ok(Value::bool(true))),
+        "false" => CompiledExpr::new(move |_| Ok(Value::bool(false))),
         "Bool" => CompiledExpr::new(move |_| {
-            Ok(Value::Set(ImmutableSet::from(vec![
-                Value::Bool(true),
-                Value::Bool(false),
+            Ok(Value::set(ImmutableSet::from(vec![
+                Value::bool(true),
+                Value::bool(false),
             ])))
         }),
         _ => unimplemented!("Unknown builtin name: {}", name),
diff --git a/evaluator/src/itf.rs b/evaluator/src/itf.rs
index 16fc1931f..e3b770d91 100644
--- a/evaluator/src/itf.rs
+++ b/evaluator/src/itf.rs
@@ -5,7 +5,7 @@
 //! This format can be parsed by Quint's typescript tool and by the ITF trace
 //! viewer extension on VSCode.
 
-use crate::value::Value;
+use crate::value::{Value, ValueInner};
 use chrono::{self};
 use itf;
 use std::collections::BTreeMap;
@@ -33,10 +33,14 @@ impl Trace {
 
         // Find the variable names by taking the fields from the first state
         // (which should be a record)
-        let vars = if let Some(Value::Record(map)) = self.states.first() {
-            map.keys().map(|v| v.to_string()).collect::<Vec<_>>()
+        let vars = if let Some(first_state) = self.states.first() {
+            if let ValueInner::Record(map) = first_state.0.as_ref() {
+                map.keys().map(|v| v.to_string()).collect::<Vec<_>>()
+            } else {
+                panic!("Expected a record, got {}", self.states[0]);
+            }
         } else {
-            panic!("Expected a record, got {}", self.states[0]);
+            panic!("No states found");
         };
 
         let mut other = BTreeMap::new();
@@ -74,29 +78,31 @@ impl Trace {
 
 impl Value {
     pub fn to_itf(&self) -> itf::Value {
-        match self {
-            Self::Int(i) => itf::Value::Number(*i),
-            Self::Bool(b) => itf::Value::Bool(*b),
-            Self::Str(s) => itf::Value::String(s.to_string()),
-            Self::Set(_)
-            | Self::Interval(_, _)
-            | Self::CrossProduct(_)
-            | Self::PowerSet(_)
-            | Self::MapSet(_, _) => {
+        match self.0.as_ref() {
+            ValueInner::Int(i) => itf::Value::Number(*i),
+            ValueInner::Bool(b) => itf::Value::Bool(*b),
+            ValueInner::Str(s) => itf::Value::String(s.to_string()),
+            ValueInner::Set(_)
+            | ValueInner::Interval(_, _)
+            | ValueInner::CrossProduct(_)
+            | ValueInner::PowerSet(_)
+            | ValueInner::MapSet(_, _) => {
                 itf::Value::Set(self.as_set().iter().map(|v| v.to_itf()).collect())
             }
-            Self::Tuple(elems) => itf::Value::Tuple(elems.iter().map(|v| v.to_itf()).collect()),
-            Self::Record(fields) => itf::Value::Record(
+            ValueInner::Tuple(elems) => {
+                itf::Value::Tuple(elems.iter().map(|v| v.to_itf()).collect())
+            }
+            ValueInner::Record(fields) => itf::Value::Record(
                 fields
                     .iter()
                     .map(|(k, v)| (k.to_string(), v.to_itf()))
                     .collect(),
             ),
-            Self::Map(map) => {
+            ValueInner::Map(map) => {
                 itf::Value::Map(map.iter().map(|(k, v)| (k.to_itf(), v.to_itf())).collect())
             }
-            Self::List(elems) => itf::Value::List(elems.iter().map(|v| v.to_itf()).collect()),
-            Self::Variant(label, value) => itf::Value::Record(
+            ValueInner::List(elems) => itf::Value::List(elems.iter().map(|v| v.to_itf()).collect()),
+            ValueInner::Variant(label, value) => itf::Value::Record(
                 vec![
                     ("tag".to_string(), itf::Value::String(label.to_string())),
                     ("value".to_string(), value.to_itf()),
@@ -104,7 +110,7 @@ impl Value {
                 .into_iter()
                 .collect(),
             ),
-            Self::Lambda(_, _) => panic!("Cannot convert Lambda to ITF"),
+            ValueInner::Lambda(_, _) => panic!("Cannot convert Lambda to ITF"),
         }
     }
 }
diff --git a/evaluator/src/nondet.rs b/evaluator/src/nondet.rs
index 9c2584937..ff5a5720d 100644
--- a/evaluator/src/nondet.rs
+++ b/evaluator/src/nondet.rs
@@ -6,7 +6,7 @@
 use crate::{
     evaluator::{CompiledExpr, Env},
     ir::QuintError,
-    value::Value,
+    value::{Value, ValueInner},
 };
 use std::cell::RefCell;
 use std::rc::Rc;
@@ -71,7 +71,7 @@ pub fn eval_nondet_one_of(
         let bounds = set.bounds();
         for bound in &bounds {
             if *bound == 0 {
-                return Ok(Value::Bool(false));
+                return Ok(Value::bool(false));
             }
         }
 
@@ -93,7 +93,8 @@ pub fn eval_nondet_one_of(
             let result = body_expr.execute(env);
 
             // If result is false and we can retry, try next position
-            let should_retry = matches!(result, Ok(Value::Bool(false))) && should_retry_set;
+            let should_retry = matches!(result, Ok(ref v) if matches!(v.0.as_ref(), ValueInner::Bool(false)))
+                && should_retry_set;
 
             if should_retry {
                 // Increment positions to try next combination
diff --git a/evaluator/src/normalizer.rs b/evaluator/src/normalizer.rs
index edeb21233..11114f4e2 100644
--- a/evaluator/src/normalizer.rs
+++ b/evaluator/src/normalizer.rs
@@ -2,42 +2,45 @@
 //! map keys and set elements, to make sure we don't end up with something like
 //! `Map(Set(1, 2, 3) -> "a", 1.to(3) -> "b")` (the two keys are the same).
 
-use crate::value::Value;
-use std::rc::Rc;
+use crate::value::{Value, ValueInner};
 
 impl Value {
     #[allow(clippy::unnecessary_to_owned)]
     pub fn normalize(self) -> Value {
-        match self {
-            Value::Int(_) | Value::Bool(_) | Value::Str(_) => self,
-            Value::Set(_)
-            | Value::Interval(_, _)
-            | Value::CrossProduct(_)
-            | Value::PowerSet(_)
-            | Value::MapSet(_, _) => Value::Set(
+        match self.0.as_ref() {
+            ValueInner::Int(_) | ValueInner::Bool(_) | ValueInner::Str(_) => self,
+            ValueInner::Set(_)
+            | ValueInner::Interval(_, _)
+            | ValueInner::CrossProduct(_)
+            | ValueInner::PowerSet(_)
+            | ValueInner::MapSet(_, _) => Value::set(
                 self.as_set()
                     .into_owned()
                     .into_iter()
                     .map(|v| v.normalize())
                     .collect(),
             ),
-            Value::Tuple(elems) => Value::Tuple(elems.into_iter().map(|v| v.normalize()).collect()),
-            Value::Record(fields) => Value::Record(
+            ValueInner::Tuple(elems) => {
+                Value::tuple(elems.iter().cloned().map(|v| v.normalize()).collect())
+            }
+            ValueInner::Record(fields) => Value::record(
                 fields
-                    .into_iter()
-                    .map(|(k, v)| (k, v.normalize()))
+                    .iter()
+                    .map(|(k, v)| (k.clone(), v.clone().normalize()))
                     .collect(),
             ),
-            Value::Map(map) => Value::Map(
-                map.into_iter()
-                    .map(|(k, v)| (k.normalize(), v.normalize()))
+            ValueInner::Map(map) => Value::map(
+                map.iter()
+                    .map(|(k, v)| (k.clone().normalize(), v.clone().normalize()))
                     .collect(),
             ),
-            Value::List(elems) => Value::List(elems.into_iter().map(|v| v.normalize()).collect()),
-            Value::Variant(label, value) => {
-                Value::Variant(label, Rc::new(<Value as Clone>::clone(&value).normalize()))
+            ValueInner::List(elems) => {
+                Value::list(elems.iter().cloned().map(|v| v.normalize()).collect())
+            }
+            ValueInner::Variant(label, value) => {
+                Value::variant(label.clone(), value.clone().normalize())
             }
-            Value::Lambda(_, _) => panic!("Cannot normalize lambda"),
+            ValueInner::Lambda(_, _) => panic!("Cannot normalize lambda"),
         }
     }
 }
diff --git a/evaluator/src/picker.rs b/evaluator/src/picker.rs
index f147c0945..ad7b69ea5 100644
--- a/evaluator/src/picker.rs
+++ b/evaluator/src/picker.rs
@@ -1,7 +1,7 @@
 //! Picking values out of sets without enumerating the elements.
 
-use crate::value::{powerset_at_index, ImmutableMap, Value};
-use std::{convert::TryInto, rc::Rc};
+use crate::value::{powerset_at_index, ImmutableMap, Value, ValueInner};
+use std::convert::TryInto;
 
 impl Value {
     /// Pick a value from the set, using the given indexes, without enumerating
@@ -10,46 +10,46 @@ impl Value {
     /// The given indexes should have the same length as the length [`bounds`]
     /// for this value, and each value should be within its respective bound.
     pub fn pick<T: Iterator<Item = usize>>(&self, indexes: &mut T) -> Value {
-        match self {
-            Value::Set(set) => {
+        match self.0.as_ref() {
+            ValueInner::Set(set) => {
                 let index = indexes
                     .next()
                     .expect("Internal error: too few positions. Report a bug");
                 set.iter().collect::<Vec<_>>()[index].clone()
             }
-            Value::Interval(start, end) => {
+            ValueInner::Interval(start, end) => {
                 let index = indexes
                     .next()
                     .expect("Internal error: too few positions. Report a bug");
                 let idx: i64 = <usize as TryInto<i64>>::try_into(index).unwrap();
                 assert!(idx <= end - start);
-                Value::Int(start + idx)
+                Value::int(start + idx)
             }
-            Value::CrossProduct(sets) => {
-                Value::Tuple(sets.iter().map(|value| value.pick(indexes)).collect())
+            ValueInner::CrossProduct(sets) => {
+                Value::tuple(sets.iter().map(|value| value.pick(indexes)).collect())
             }
-            Value::PowerSet(base_set) => {
+            ValueInner::PowerSet(base_set) => {
                 let index = indexes
                     .next()
                     .expect("Internal error: too few positions. Report a bug");
                 powerset_at_index(&base_set.as_set(), index)
             }
-            Value::MapSet(domain, range) => {
+            ValueInner::MapSet(domain, range) => {
                 let domain_size = domain.cardinality();
                 let range_size = range.cardinality();
 
                 if domain_size == 0 {
                     // To reflect the behaviour of TLC, an empty domain needs to give Set(Map()),
                     // so the only element we can pick is Map().
-                    return Value::Map(ImmutableMap::default());
+                    return Value::map(ImmutableMap::default());
                 }
 
                 assert!(range_size > 0, "Range can't be zero");
 
-                let range_to_pick = if let Value::MapSet(_, _) = **range {
-                    Rc::new(Value::Set(range.as_set().into_owned()))
+                let range_to_pick = if matches!(range.0.as_ref(), ValueInner::MapSet(_, _)) {
+                    Value::set(range.as_set().into_owned())
                 } else {
-                    Rc::clone(range)
+                    range.clone()
                 };
 
                 let keys = domain.as_set();
@@ -58,7 +58,7 @@ impl Value {
                     (key.clone(), value)
                 });
 
-                Value::Map(ImmutableMap::from_iter(key_values))
+                Value::map(ImmutableMap::from_iter(key_values))
             }
             _ => panic!("Not a set"),
         }
@@ -69,12 +69,12 @@ impl Value {
     // (set1.pick(r1), set2.pick(r2), ..., setn.pick(rn)). The `bounds` function will return the list of
     // ranges (bounds) from which each of those numbers should be picked from.
     pub fn bounds(&self) -> Vec<usize> {
-        match self {
-            Value::Set(set) => vec![set.len()],
-            Value::Interval(_, _) => vec![self.cardinality()],
-            Value::CrossProduct(sets) => sets.iter().map(|set| set.cardinality()).collect(),
-            Value::PowerSet(base_set) => vec![base_set.cardinality()],
-            Value::MapSet(domain, range) => {
+        match self.0.as_ref() {
+            ValueInner::Set(set) => vec![set.len()],
+            ValueInner::Interval(_, _) => vec![self.cardinality()],
+            ValueInner::CrossProduct(sets) => sets.iter().map(|set| set.cardinality()).collect(),
+            ValueInner::PowerSet(base_set) => vec![base_set.cardinality()],
+            ValueInner::MapSet(domain, range) => {
                 // Cardinality of range repeated domain times
                 vec![range.cardinality(); domain.cardinality()]
             }
diff --git a/evaluator/src/storage.rs b/evaluator/src/storage.rs
index 1acd193ad..83b908a0f 100644
--- a/evaluator/src/storage.rs
+++ b/evaluator/src/storage.rs
@@ -69,7 +69,7 @@ impl Storage {
         });
 
         // TODO: add nondet picks and action taken
-        Value::Record(ImmutableMap::from_iter(map))
+        Value::record(ImmutableMap::from_iter(map))
     }
 
     pub fn take_snapshot(&self) -> Snapshot {
diff --git a/evaluator/src/value.rs b/evaluator/src/value.rs
index fa1a8921b..b79fd37be 100644
--- a/evaluator/src/value.rs
+++ b/evaluator/src/value.rs
@@ -25,6 +25,7 @@ use std::borrow::Cow;
 use std::cell::RefCell;
 use std::fmt;
 use std::hash::{Hash, Hasher};
+use std::ops::Deref;
 use std::rc::Rc;
 
 /// Quint values that hold sets are immutable, use `GenericHashSet` immutable
@@ -43,11 +44,15 @@ pub type ImmutableMap<K, V> = GenericHashMap<K, V, fxhash::FxBuildHasher, RcK>;
 pub type Str = hipstr::HipStr<'static>;
 
 /// A Quint value produced by evaluation of a Quint expression.
-///
+/// Values are immutable and reference-counted for cheap cloning.
+#[derive(Clone, Debug)]
+pub struct Value(pub Rc<ValueInner>);
+
+/// The actual value enum wrapped in Rc for cheap cloning.
 /// Can be seen as a normal form of the expression, except for the intermediate
 /// values that enable lazy evaluation of some potentially expensive expressions.
-#[derive(Clone, Debug)]
-pub enum Value {
+#[derive(Debug, Clone)]
+pub enum ValueInner {
     Int(i64),
     Bool(bool),
     Str(Str),
@@ -57,15 +62,21 @@ pub enum Value {
     Map(ImmutableMap<Value, Value>),
     List(ImmutableVec<Value>),
     Lambda(Vec<Rc<RefCell<EvalResult>>>, CompiledExpr),
-    Variant(QuintName, Rc<Value>),
+    Variant(QuintName, Value),
     // "Intermediate" values using during evaluation to avoid expensive computations
     Interval(i64, i64),
     CrossProduct(Vec<Value>),
-    PowerSet(Rc<Value>),
-    MapSet(Rc<Value>, Rc<Value>),
+    PowerSet(Value),
+    MapSet(Value, Value),
 }
 
 impl Hash for Value {
+    fn hash<H: Hasher>(&self, state: &mut H) {
+        self.0.as_ref().hash(state);
+    }
+}
+
+impl Hash for ValueInner {
     fn hash<H: Hasher>(&self, state: &mut H) {
         // First, hash the discriminant, as we want hashes of Set(1, 2, 3) and
         // List(1, 2, 3) to be different.
@@ -73,56 +84,56 @@ impl Hash for Value {
         discr.hash(state);
 
         match self {
-            Value::Int(n) => n.hash(state),
-            Value::Bool(b) => b.hash(state),
-            Value::Str(s) => s.hash(state),
-            Value::Set(set) => {
+            ValueInner::Int(n) => n.hash(state),
+            ValueInner::Bool(b) => b.hash(state),
+            ValueInner::Str(s) => s.hash(state),
+            ValueInner::Set(set) => {
                 for elem in set {
                     elem.hash(state);
                 }
             }
-            Value::Tuple(elems) => {
+            ValueInner::Tuple(elems) => {
                 for elem in elems {
                     elem.hash(state);
                 }
             }
-            Value::Record(fields) => {
+            ValueInner::Record(fields) => {
                 for (name, value) in fields {
                     name.hash(state);
                     value.hash(state);
                 }
             }
-            Value::Map(map) => {
+            ValueInner::Map(map) => {
                 for (key, value) in map {
                     key.hash(state);
                     value.hash(state);
                 }
             }
-            Value::List(elems) => {
+            ValueInner::List(elems) => {
                 for elem in elems {
                     elem.hash(state);
                 }
             }
-            Value::Lambda(_, _) => {
+            ValueInner::Lambda(_, _) => {
                 panic!("Cannot hash lambda");
             }
-            Value::Variant(label, value) => {
+            ValueInner::Variant(label, value) => {
                 label.hash(state);
                 value.hash(state);
             }
-            Value::Interval(start, end) => {
+            ValueInner::Interval(start, end) => {
                 start.hash(state);
                 end.hash(state);
             }
-            Value::CrossProduct(sets) => {
+            ValueInner::CrossProduct(sets) => {
                 for value in sets {
                     value.hash(state);
                 }
             }
-            Value::PowerSet(value) => {
+            ValueInner::PowerSet(value) => {
                 value.hash(state);
             }
-            Value::MapSet(a, b) => {
+            ValueInner::MapSet(a, b) => {
                 a.hash(state);
                 b.hash(state);
             }
@@ -131,52 +142,132 @@ impl Hash for Value {
 }
 
 impl PartialEq for Value {
+    fn eq(&self, other: &Self) -> bool {
+        self.0.as_ref() == other.0.as_ref()
+    }
+}
+
+impl PartialEq for ValueInner {
     fn eq(&self, other: &Self) -> bool {
         match (self, other) {
-            (Value::Int(a), Value::Int(b)) => a == b,
-            (Value::Bool(a), Value::Bool(b)) => a == b,
-            (Value::Str(a), Value::Str(b)) => a == b,
-            (Value::Set(a), Value::Set(b)) => *a == *b,
-            (Value::Tuple(a), Value::Tuple(b)) => *a == *b,
-            (Value::Record(a), Value::Record(b)) => *a == *b,
-            (Value::Map(a), Value::Map(b)) => *a == *b,
-            (Value::List(a), Value::List(b)) => *a == *b,
-            (Value::Lambda(_, _), Value::Lambda(_, _)) => panic!("Cannot compare lambdas"),
-            (Value::Variant(a_label, a_value), Value::Variant(b_label, b_value)) => {
+            (Self::Int(a), Self::Int(b)) => a == b,
+            (Self::Bool(a), Self::Bool(b)) => a == b,
+            (Self::Str(a), Self::Str(b)) => a == b,
+            (Self::Set(a), Self::Set(b)) => *a == *b,
+            (Self::Tuple(a), Self::Tuple(b)) => *a == *b,
+            (Self::Record(a), Self::Record(b)) => *a == *b,
+            (Self::Map(a), Self::Map(b)) => *a == *b,
+            (Self::List(a), Self::List(b)) => *a == *b,
+            (Self::Lambda(_, _), Self::Lambda(_, _)) => panic!("Cannot compare lambdas"),
+            (Self::Variant(a_label, a_value), Self::Variant(b_label, b_value)) => {
                 a_label == b_label && a_value == b_value
             }
-            (Value::Interval(a_start, a_end), Value::Interval(b_start, b_end)) => {
+            (Self::Interval(a_start, a_end), Self::Interval(b_start, b_end)) => {
                 a_start == b_start && a_end == b_end
             }
-            (Value::CrossProduct(a), Value::CrossProduct(b)) => *a == *b,
-            (Value::PowerSet(a), Value::PowerSet(b)) => *a == *b,
-            (Value::MapSet(a1, b1), Value::MapSet(a2, b2)) => a1 == a2 && b1 == b2,
+            (Self::CrossProduct(a), Self::CrossProduct(b)) => *a == *b,
+            (Self::PowerSet(a), Self::PowerSet(b)) => *a == *b,
+            (Self::MapSet(a1, b1), Self::MapSet(a2, b2)) => a1 == a2 && b1 == b2,
             // To compare two sets represented in different ways, we need to enumerate them both
-            (a, b) if a.is_set() && b.is_set() => a.as_set() == b.as_set(),
-            _ => false,
+            _ => {
+                let self_value = Value(Rc::new(self.clone()));
+                let other_value = Value(Rc::new(other.clone()));
+                if self_value.is_set() && other_value.is_set() {
+                    self_value.as_set() == other_value.as_set()
+                } else {
+                    false
+                }
+            }
         }
     }
 }
 
 impl Eq for Value {}
+impl Eq for ValueInner {}
+
+impl Deref for Value {
+    type Target = ValueInner;
+
+    fn deref(&self) -> &Self::Target {
+        &self.0
+    }
+}
 
 impl Value {
+    // Constructor functions for Value
+    pub fn int(n: i64) -> Self {
+        Value(Rc::new(ValueInner::Int(n)))
+    }
+
+    pub fn bool(b: bool) -> Self {
+        Value(Rc::new(ValueInner::Bool(b)))
+    }
+
+    pub fn str(s: Str) -> Self {
+        Value(Rc::new(ValueInner::Str(s)))
+    }
+
+    pub fn set(s: ImmutableSet<Value>) -> Self {
+        Value(Rc::new(ValueInner::Set(s)))
+    }
+
+    pub fn tuple(t: ImmutableVec<Value>) -> Self {
+        Value(Rc::new(ValueInner::Tuple(t)))
+    }
+
+    pub fn record(r: ImmutableMap<QuintName, Value>) -> Self {
+        Value(Rc::new(ValueInner::Record(r)))
+    }
+
+    pub fn map(m: ImmutableMap<Value, Value>) -> Self {
+        Value(Rc::new(ValueInner::Map(m)))
+    }
+
+    pub fn list(l: ImmutableVec<Value>) -> Self {
+        Value(Rc::new(ValueInner::List(l)))
+    }
+
+    pub fn lambda(registers: Vec<Rc<RefCell<EvalResult>>>, body: CompiledExpr) -> Self {
+        Value(Rc::new(ValueInner::Lambda(registers, body)))
+    }
+
+    pub fn variant(name: QuintName, value: Value) -> Self {
+        Value(Rc::new(ValueInner::Variant(name, value)))
+    }
+
+    pub fn interval(start: i64, end: i64) -> Self {
+        Value(Rc::new(ValueInner::Interval(start, end)))
+    }
+
+    pub fn cross_product(values: Vec<Value>) -> Self {
+        Value(Rc::new(ValueInner::CrossProduct(values)))
+    }
+
+    pub fn power_set(value: Value) -> Self {
+        Value(Rc::new(ValueInner::PowerSet(value)))
+    }
+
+    pub fn map_set(a: Value, b: Value) -> Self {
+        Value(Rc::new(ValueInner::MapSet(a, b)))
+    }
     /// Calculate the cardinality of the value without having to enumerate it
     /// (i.e. without calling `as_set`).
     pub fn cardinality(&self) -> usize {
-        match self {
-            Value::Set(set) => set.len(),
-            Value::Tuple(elems) => elems.len(),
-            Value::Record(fields) => fields.len(),
-            Value::Map(map) => map.len(),
-            Value::List(elems) => elems.len(),
-            Value::Interval(start, end) => (end - start + 1).try_into().unwrap(),
-            Value::CrossProduct(sets) => sets.iter().fold(1, |acc, set| acc * set.cardinality()),
-            Value::PowerSet(value) => {
+        match self.0.as_ref() {
+            ValueInner::Set(set) => set.len(),
+            ValueInner::Tuple(elems) => elems.len(),
+            ValueInner::Record(fields) => fields.len(),
+            ValueInner::Map(map) => map.len(),
+            ValueInner::List(elems) => elems.len(),
+            ValueInner::Interval(start, end) => (end - start + 1).try_into().unwrap(),
+            ValueInner::CrossProduct(sets) => {
+                sets.iter().fold(1, |acc, set| acc * set.cardinality())
+            }
+            ValueInner::PowerSet(value) => {
                 // 2^(cardinality of value)
                 2_usize.pow(value.cardinality().try_into().unwrap())
             }
-            Value::MapSet(domain, range) => {
+            ValueInner::MapSet(domain, range) => {
                 // (cardinality of range)^(cardinality of domain()
                 range
                     .cardinality()
@@ -189,22 +280,22 @@ impl Value {
     /// Check for membership of a value in a set, without having to enumerate
     /// the set.
     pub fn contains(&self, elem: &Value) -> bool {
-        match (self, elem) {
-            (Value::Set(elems), _) => elems.contains(elem),
-            (Value::Interval(start, end), Value::Int(n)) => start <= n && n <= end,
-            (Value::CrossProduct(sets), Value::Tuple(elems)) => {
+        match (self.0.as_ref(), elem.0.as_ref()) {
+            (ValueInner::Set(elems), _) => elems.contains(elem),
+            (ValueInner::Interval(start, end), ValueInner::Int(n)) => start <= n && n <= end,
+            (ValueInner::CrossProduct(sets), ValueInner::Tuple(elems)) => {
                 sets.len() == elems.len()
                     && sets.iter().zip(elems).all(|(set, elem)| set.contains(elem))
             }
-            (Value::PowerSet(base), Value::Set(elems)) => {
+            (ValueInner::PowerSet(base), ValueInner::Set(elems)) => {
                 let base_elems = base.as_set();
                 elems.len() <= base_elems.len()
                     && elems.iter().all(|elem| base_elems.contains(elem))
             }
-            (Value::MapSet(domain, range), Value::Map(map)) => {
-                let map_domain = Value::Set(map.keys().cloned().collect::<ImmutableSet<_>>());
+            (ValueInner::MapSet(domain, range), ValueInner::Map(map)) => {
+                let map_domain = Value::set(map.keys().cloned().collect::<ImmutableSet<_>>());
                 // Check if domains are equal and all map values are in the range set
-                map_domain == **domain && map.values().all(|v| range.contains(v))
+                map_domain == *domain && map.values().all(|v| range.contains(v))
             }
             _ => panic!("contains not implemented for {self:?}"),
         }
@@ -212,34 +303,36 @@ impl Value {
 
     /// Check if a set is a subset of another set, avoiding enumeration when possible
     pub fn subseteq(&self, superset: &Value) -> bool {
-        match (self, superset) {
-            (Value::Set(subset), Value::Set(superset)) => subset.is_subset(superset),
+        match (self.0.as_ref(), superset.0.as_ref()) {
+            (ValueInner::Set(subset), ValueInner::Set(superset)) => subset.is_subset(superset),
             (
-                Value::Interval(subset_start, subset_end),
-                Value::Interval(superset_start, superset_end),
+                ValueInner::Interval(subset_start, subset_end),
+                ValueInner::Interval(superset_start, superset_end),
             ) => subset_start >= superset_start && subset_end <= superset_end,
-            (Value::CrossProduct(subsets), Value::CrossProduct(supersets)) => {
+            (ValueInner::CrossProduct(subsets), ValueInner::CrossProduct(supersets)) => {
                 subsets.len() == supersets.len()
                     && subsets
                         .iter()
                         .zip(supersets)
                         .all(|(subset, superset)| subset.subseteq(superset))
             }
-            (Value::PowerSet(subset), Value::PowerSet(superset)) => subset.subseteq(superset),
+            (ValueInner::PowerSet(subset), ValueInner::PowerSet(superset)) => {
+                subset.subseteq(superset)
+            }
             (
-                Value::MapSet(subset_domain, subset_range),
-                Value::MapSet(superset_domain, superset_range),
+                ValueInner::MapSet(subset_domain, subset_range),
+                ValueInner::MapSet(superset_domain, superset_range),
             ) => subset_domain == superset_domain && subset_range.subseteq(superset_range),
             // Fall back to the native implementation (`is_subset`) if no optimization is possible
-            (subset, superset) => subset.as_set().is_subset(superset.as_set().as_ref()),
+            (_, _) => self.as_set().is_subset(superset.as_set().as_ref()),
         }
     }
 
     /// Convert an integer value to `i64`. Panics if the wrong type is given,
     /// which should never happen as input expressions are type-checked.
     pub fn as_int(&self) -> i64 {
-        match self {
-            Value::Int(n) => *n,
+        match self.0.as_ref() {
+            ValueInner::Int(n) => *n,
             _ => panic!("Expected integer"),
         }
     }
@@ -247,8 +340,8 @@ impl Value {
     /// Convert a boolean value to `bool`. Panics if the wrong type is given,
     /// which should never happen as input expressions are type-checked.
     pub fn as_bool(&self) -> bool {
-        match self {
-            Value::Bool(b) => *b,
+        match self.0.as_ref() {
+            ValueInner::Bool(b) => *b,
             _ => panic!("Expected boolean"),
         }
     }
@@ -256,8 +349,8 @@ impl Value {
     /// Convert a string value to `Str`. Panics if the wrong type is given,
     /// which should never happen as input expressions are type-checked.
     pub fn as_str(&self) -> Str {
-        match self {
-            Value::Str(s) => s.clone(),
+        match self.0.as_ref() {
+            ValueInner::Str(s) => s.clone(),
             _ => panic!("Expected string"),
         }
     }
@@ -266,12 +359,12 @@ impl Value {
     /// that are also sets, just not enumerated yet.
     pub fn is_set(&self) -> bool {
         matches!(
-            self,
-            Value::Set(_)
-                | Value::Interval(_, _)
-                | Value::CrossProduct(_)
-                | Value::PowerSet(_)
-                | Value::MapSet(_, _)
+            self.0.as_ref(),
+            ValueInner::Set(_)
+                | ValueInner::Interval(_, _)
+                | ValueInner::CrossProduct(_)
+                | ValueInner::PowerSet(_)
+                | ValueInner::MapSet(_, _)
         )
     }
 
@@ -283,10 +376,12 @@ impl Value {
     /// clone-on-write (Cow) pointer, avoiding unnecessary clones that would be
     /// required if we always wanted to return Owned data.
     pub fn as_set(&self) -> Cow<'_, ImmutableSet<Value>> {
-        match self {
-            Value::Set(set) => Cow::Borrowed(set),
-            Value::Interval(start, end) => Cow::Owned((*start..=*end).map(Value::Int).collect()),
-            Value::CrossProduct(sets) => {
+        match self.0.as_ref() {
+            ValueInner::Set(set) => Cow::Borrowed(set),
+            ValueInner::Interval(start, end) => {
+                Cow::Owned((*start..=*end).map(Value::int).collect())
+            }
+            ValueInner::CrossProduct(sets) => {
                 let size = self.cardinality();
                 if size == 0 {
                     // an empty set produces the empty product
@@ -298,13 +393,13 @@ impl Value {
                     .iter()
                     .map(|set| set.as_set().into_owned().into_iter().collect::<Vec<_>>())
                     .multi_cartesian_product()
-                    .map(|product| Value::Tuple(ImmutableVec::from(product)))
+                    .map(|product| Value::tuple(ImmutableVec::from(product)))
                     .collect::<ImmutableSet<_>>();
 
                 Cow::Owned(product_sets)
             }
 
-            Value::PowerSet(value) => {
+            ValueInner::PowerSet(value) => {
                 let base = value.as_set();
                 let size = 1 << base.len(); // 2^n subsets for a set of size n
                 Cow::Owned(
@@ -314,11 +409,11 @@ impl Value {
                 )
             }
 
-            Value::MapSet(domain, range) => {
+            ValueInner::MapSet(domain, range) => {
                 if domain.cardinality() == 0 {
                     // To reflect the behaviour of TLC, an empty domain needs to give Set(Map())
                     return Cow::Owned(
-                        std::iter::once(Value::Map(ImmutableMap::default())).collect(),
+                        std::iter::once(Value::map(ImmutableMap::default())).collect(),
                     );
                 }
 
@@ -343,7 +438,7 @@ impl Value {
                         pairs.push((key.clone(), range_vec[index % nvalues].clone()));
                         index /= nvalues;
                     }
-                    result_set.insert(Value::Map(ImmutableMap::from_iter(pairs)));
+                    result_set.insert(Value::map(ImmutableMap::from_iter(pairs)));
                 }
 
                 Cow::Owned(result_set)
@@ -355,8 +450,8 @@ impl Value {
     /// Convert a map value to a map. Panics if the wrong type is given, which
     /// should never happen as input expressions are type-checked.
     pub fn as_map(&self) -> &ImmutableMap<Value, Value> {
-        match self {
-            Value::Map(map) => map,
+        match self.0.as_ref() {
+            ValueInner::Map(map) => map,
             _ => panic!("Expected map"),
         }
     }
@@ -364,9 +459,9 @@ impl Value {
     /// Convert a list or a tuple value to a vector. Panics if the wrong type is
     /// given, which should never happen as input expressions are type-checked.
     pub fn as_list(&self) -> &ImmutableVec<Value> {
-        match self {
-            Value::Tuple(elems) => elems,
-            Value::List(elems) => elems,
+        match self.0.as_ref() {
+            ValueInner::Tuple(elems) => elems,
+            ValueInner::List(elems) => elems,
             _ => panic!("Expected list, got {self:?}"),
         }
     }
@@ -374,8 +469,8 @@ impl Value {
     /// Convert a record value to a map. Panics if the wrong type is given,
     /// which should never happen as input expressions are type-checked.
     pub fn as_record_map(&self) -> &ImmutableMap<QuintName, Value> {
-        match self {
-            Value::Record(fields) => fields,
+        match self.0.as_ref() {
+            ValueInner::Record(fields) => fields,
             _ => panic!("Expected record"),
         }
     }
@@ -383,8 +478,8 @@ impl Value {
     /// Convert a lambda value to a closure. Panics if the wrong type is given,
     /// which should never happen as input expressions are type-checked.
     pub fn as_closure(&self) -> impl Fn(&mut Env, Vec<Value>) -> EvalResult + '_ {
-        match self {
-            Value::Lambda(registers, body) => move |env: &mut Env, args: Vec<Value>| {
+        match self.0.as_ref() {
+            ValueInner::Lambda(registers, body) => move |env: &mut Env, args: Vec<Value>| {
                 args.into_iter().enumerate().for_each(|(i, arg)| {
                     *registers[i].borrow_mut() = Ok(arg);
                 });
@@ -400,8 +495,8 @@ impl Value {
     /// wrong type is given, which should never happen as input expressions are
     /// type-checked.
     pub fn as_variant(&self) -> (&QuintName, &Value) {
-        match self {
-            Value::Variant(label, value) => (label, value),
+        match self.0.as_ref() {
+            ValueInner::Variant(label, value) => (label, value),
             _ => panic!("Expected variant"),
         }
     }
@@ -436,21 +531,21 @@ pub fn powerset_at_index(base: &ImmutableSet<Value>, i: usize) -> Value {
             elems.insert(elem.clone());
         }
     }
-    Value::Set(elems)
+    Value::set(elems)
 }
 
 /// Display implementation, used for debugging only. Users should not need to see a [`Value`].
 impl fmt::Display for Value {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> std::fmt::Result {
-        match self {
-            Value::Int(n) => write!(f, "{n}"),
-            Value::Bool(b) => write!(f, "{b}"),
-            Value::Str(s) => write!(f, "{s:?}"),
-            Value::Set(_)
-            | Value::Interval(_, _)
-            | Value::CrossProduct(_)
-            | Value::PowerSet(_)
-            | Value::MapSet(_, _) => {
+        match self.0.as_ref() {
+            ValueInner::Int(n) => write!(f, "{n}"),
+            ValueInner::Bool(b) => write!(f, "{b}"),
+            ValueInner::Str(s) => write!(f, "{s:?}"),
+            ValueInner::Set(_)
+            | ValueInner::Interval(_, _)
+            | ValueInner::CrossProduct(_)
+            | ValueInner::PowerSet(_)
+            | ValueInner::MapSet(_, _) => {
                 write!(f, "Set(")?;
                 for (i, set) in self.as_set().iter().enumerate() {
                     if i > 0 {
@@ -460,7 +555,7 @@ impl fmt::Display for Value {
                 }
                 write!(f, ")")
             }
-            Value::Tuple(elems) => {
+            ValueInner::Tuple(elems) => {
                 write!(f, "(")?;
                 for (i, elem) in elems.iter().enumerate() {
                     if i > 0 {
@@ -470,7 +565,7 @@ impl fmt::Display for Value {
                 }
                 write!(f, ")")
             }
-            Value::Record(fields) => {
+            ValueInner::Record(fields) => {
                 write!(f, "{{ ")?;
                 for (i, (name, value)) in fields.iter().enumerate() {
                     if i > 0 {
@@ -480,7 +575,7 @@ impl fmt::Display for Value {
                 }
                 write!(f, " }}")
             }
-            Value::Map(map) => {
+            ValueInner::Map(map) => {
                 write!(f, "Map(")?;
                 for (i, (key, value)) in map.iter().enumerate() {
                     if i > 0 {
@@ -490,7 +585,7 @@ impl fmt::Display for Value {
                 }
                 write!(f, ")")
             }
-            Value::List(elems) => {
+            ValueInner::List(elems) => {
                 write!(f, "List(")?;
                 for (i, elem) in elems.iter().enumerate() {
                     if i > 0 {
@@ -500,9 +595,9 @@ impl fmt::Display for Value {
                 }
                 write!(f, ")")
             }
-            Value::Lambda(_, _) => write!(f, "<lambda>"),
-            Value::Variant(label, value) => {
-                if let Value::Tuple(elems) = &**value {
+            ValueInner::Lambda(_, _) => write!(f, "<lambda>"),
+            ValueInner::Variant(label, value) => {
+                if let ValueInner::Tuple(elems) = value.0.as_ref() {
                     if elems.is_empty() {
                         return write!(f, "{label}");
                     }
@@ -512,3 +607,18 @@ impl fmt::Display for Value {
         }
     }
 }
+
+// NOTE: The `Value` data structure is used within immutable containers from the
+// `imbl` crate. Those containers have optimizations that are well suited for
+// small datas tructures. For example, vectors are represented as RRB trees but,
+// the space that an RRB tree would occupy in the stack is first used by an
+// array that can hold a portion of the vector elements inline before promoting
+// them to a RRB tree. This means that the larger the `Value` structure is, the
+// quicker the RRB tree promotion needs to happen, which requires additional
+// heap allocations.
+//
+// We've seem cosiderable performance improvements from reducing the size of the
+// `Value` representation. This compile time assertion serves as feedback to
+// developers that, if changing the size of the `Value` structure, need to make
+// sure that benchmarks don't regress.
+const _: [bool; std::mem::size_of::<Value>()] = [false; 8];
diff --git a/evaluator/tests/evaluation_tests.rs b/evaluator/tests/evaluation_tests.rs
index 7be9df0cd..b04aacfc4 100644
--- a/evaluator/tests/evaluation_tests.rs
+++ b/evaluator/tests/evaluation_tests.rs
@@ -85,7 +85,7 @@ fn assert_var_after_run(
 
     let run_result = interpreter.eval(&mut env, run_def.expr.clone());
 
-    assert_eq!(run_result, Ok(Value::Bool(true)));
+    assert_eq!(run_result, Ok(Value::bool(true)));
 
     let storage = env.var_storage.borrow();
     let var_value = storage
@@ -1077,7 +1077,7 @@ fn run_then_false_when_rhs_is_false() -> Result<(), Box<dyn std::error::Error>>
     let result = eval_run("run1", input);
 
     assert!(result.is_ok());
-    assert_eq!(result.unwrap(), Value::Bool(false));
+    assert_eq!(result.unwrap(), Value::bool(false));
 
     Ok(())
 }
@@ -1117,7 +1117,7 @@ fn run_fail() -> Result<(), Box<dyn std::error::Error>> {
                  run run1 = (n' = 1).fail()";
     let result = eval_run("run1", input);
 
-    assert_eq!(result, Ok(Value::Bool(false)));
+    assert_eq!(result, Ok(Value::bool(false)));
 
     Ok(())
 }
diff --git a/evaluator/tests/picker_tests.rs b/evaluator/tests/picker_tests.rs
index 041f88b2e..91e01de00 100644
--- a/evaluator/tests/picker_tests.rs
+++ b/evaluator/tests/picker_tests.rs
@@ -14,7 +14,7 @@ macro_rules! run_test {
         let mut env = Env::with_rand_state(interpreter.var_storage.clone(), 0x42);
 
         let init = interpreter.eval(&mut env, init_def.expr.clone());
-        assert_eq!(init.unwrap(), Value::Bool(true));
+        assert_eq!(init.unwrap(), Value::bool(true));
 
         interpreter.shift();
 
@@ -38,7 +38,7 @@ fn set_pick_test() -> Result<(), Box<dyn std::error::Error>> {
           action step = x' = x
         }";
 
-    run_test!(quint_content, Value::Int(3))
+    run_test!(quint_content, Value::int(3))
 }
 
 #[test]
@@ -53,7 +53,7 @@ fn interval_pick_test() -> Result<(), Box<dyn std::error::Error>> {
           action step = x' = x
         }";
 
-    run_test!(quint_content, Value::Int(5))
+    run_test!(quint_content, Value::int(5))
 }
 
 #[test]
@@ -75,5 +75,5 @@ fn nested_set_of_maps_pick_test() -> Result<(), Box<dyn std::error::Error>> {
           action step = myMap' = myMap
         }";
 
-    run_test!(quint_content, Value::Str("x".into()))
+    run_test!(quint_content, Value::str("x".into()))
 }
diff --git a/evaluator/tests/stateful_tests.rs b/evaluator/tests/stateful_tests.rs
index 208f5c93f..000ad1da5 100644
--- a/evaluator/tests/stateful_tests.rs
+++ b/evaluator/tests/stateful_tests.rs
@@ -14,7 +14,7 @@ macro_rules! run_test {
         let mut env = Env::with_rand_state(interpreter.var_storage.clone(), 123_456);
 
         let init = interpreter.eval(&mut env, init_def.expr.clone());
-        assert_eq!(init.unwrap(), Value::Bool(true));
+        assert_eq!(init.unwrap(), Value::bool(true));
 
         for expected_value in $expected_values {
             interpreter.shift();
@@ -24,7 +24,7 @@ macro_rules! run_test {
 
             let step_def = parsed.find_definition_by_name("step")?;
             let step = interpreter.eval(&mut env, step_def.expr.clone());
-            assert_eq!(step.unwrap(), Value::Bool(true));
+            assert_eq!(step.unwrap(), Value::bool(true));
         }
 
         Ok(())
@@ -40,7 +40,7 @@ fn assign_test() -> Result<(), Box<dyn std::error::Error>> {
           action step = x' = x + 1
         }";
 
-    run_test!(quint_content, [Value::Int(0), Value::Int(1)])
+    run_test!(quint_content, [Value::int(0), Value::int(1)])
 }
 
 #[test]
@@ -59,7 +59,7 @@ fn action_all_test() -> Result<(), Box<dyn std::error::Error>> {
           }
         }";
 
-    run_test!(quint_content, [Value::Int(2), Value::Int(5)])
+    run_test!(quint_content, [Value::int(2), Value::int(5)])
 }
 
 #[test]
@@ -79,6 +79,6 @@ fn action_any_test() -> Result<(), Box<dyn std::error::Error>> {
 
     run_test!(
         quint_content,
-        [Value::Int(2), Value::Int(8), Value::Int(32)]
+        [Value::int(2), Value::int(8), Value::int(32)]
     )
 }