diff --git a/Cargo.lock b/Cargo.lock
index 7375530a..453eaa3c 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -104,6 +104,18 @@ dependencies = [
  "typenum",
 ]
 
+[[package]]
+name = "bitvec"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1bc2832c24239b0141d5674bb9174f9d68a8b5b3f2753311927c172ca46f7e9c"
+dependencies = [
+ "funty",
+ "radium",
+ "tap",
+ "wyz",
+]
+
 [[package]]
 name = "block-buffer"
 version = "0.10.4"
@@ -118,6 +130,7 @@ name = "bounded"
 version = "0.1.0"
 dependencies = [
  "biodivine-lib-bdd",
+ "bitvec",
  "cadical",
  "fly",
  "fxhash",
@@ -460,6 +473,12 @@ dependencies = [
  "thiserror",
 ]
 
+[[package]]
+name = "funty"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6d5a32815ae3f33302d95fdcb2ce17862f8c65363dcfd29360480ba1001fc9c"
+
 [[package]]
 name = "fxhash"
 version = "0.2.1"
@@ -895,6 +914,12 @@ dependencies = [
  "proc-macro2",
 ]
 
+[[package]]
+name = "radium"
+version = "0.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dc33ff2d4973d518d823d61aa239014831e521c75da58e3df4840d3f47749d09"
+
 [[package]]
 name = "rand"
 version = "0.8.5"
@@ -1156,6 +1181,12 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "tap"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369"
+
 [[package]]
 name = "temporal-verifier"
 version = "0.1.0"
@@ -1568,6 +1599,15 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "wyz"
+version = "0.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "05f360fc0b24296329c78fda852a1e9ae82de9cf7b27dae4b7f62f118f77b9ed"
+dependencies = [
+ "tap",
+]
+
 [[package]]
 name = "yaml-rust"
 version = "0.4.5"
diff --git a/bounded/Cargo.toml b/bounded/Cargo.toml
index ae42d4fa..7410b0a8 100644
--- a/bounded/Cargo.toml
+++ b/bounded/Cargo.toml
@@ -12,3 +12,4 @@ thiserror = "1.0.40"
 biodivine-lib-bdd = "0.5.1"
 cadical = "0.1.14"
 fxhash = "0.2.1"
+bitvec = "1.0.1"
diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index 2fb79e0d..da45341e 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -4,6 +4,7 @@
 //! A bounded model checker for flyvy programs. Use `translate` to turn a flyvy `Module`
 //! into a `BoundedProgram`, then use `interpret` to evaluate it.
 
+use bitvec::prelude::*;
 use fly::{ouritertools::OurItertools, semantics::*, syntax::*, transitions::*};
 use itertools::Itertools;
 use std::collections::VecDeque;
@@ -72,7 +73,7 @@ pub fn check(
     print_timing: bool,
 ) -> Result<CheckerAnswer, TranslationError> {
     let (program, context) = translate(module, universe, print_timing)?;
-    match interpret(&program, depth, compress_traces, print_timing) {
+    match interpret(&program, depth, compress_traces, print_timing, &context) {
         InterpreterResult::Unknown => Ok(CheckerAnswer::Unknown),
         InterpreterResult::Convergence => Ok(CheckerAnswer::Convergence),
         InterpreterResult::Counterexample(trace) => {
@@ -157,38 +158,39 @@ impl Context<'_> {
 
 /// Compile-time upper bound on the bounded universe size.
 const STATE_LEN: usize = 128;
-type StateData = u8;
-const STATE_DATA_BITS: usize = std::mem::size_of::<StateData>() * 8;
 
 /// A state in the bounded system. Conceptually, this is an interpretation of the signature on the
 /// bounded universe. We represent states concretely as a bitvector, where each bit represents the
 /// presence of a tuple in a relation. The order of the bits is determined by [Context].
-#[derive(Clone, Copy, PartialEq, Eq, Hash, PartialOrd)]
-struct BoundedState([StateData; STATE_LEN / STATE_DATA_BITS]);
+#[derive(Clone, Copy, Eq, PartialOrd)]
+struct BoundedState(BitArr!(for STATE_LEN));
+
+// Go word by word instead of bit by bit.
+impl std::hash::Hash for BoundedState {
+    fn hash<H>(&self, h: &mut H)
+    where
+        H: std::hash::Hasher,
+    {
+        self.0.as_raw_slice().hash(h)
+    }
+}
+impl PartialEq for BoundedState {
+    fn eq(&self, other: &BoundedState) -> bool {
+        self.0.as_raw_slice().eq(other.0.as_raw_slice())
+    }
+}
 
 impl BoundedState {
-    const ZERO: BoundedState = BoundedState([0; STATE_LEN / STATE_DATA_BITS]);
+    const ZERO: BoundedState = BoundedState(BitArray::ZERO);
 
     fn get(&self, index: usize) -> bool {
         assert!(index < STATE_LEN, "STATE_LEN is too small");
-        let idx = index / STATE_DATA_BITS;
-        // `STATE_DATA_BITS - 1 - ` fixes ordering
-        let bit = STATE_DATA_BITS - 1 - (index % STATE_DATA_BITS);
-
-        ((self.0[idx] >> bit) & 1) != 0
+        self.0[index]
     }
 
     fn set(&mut self, index: usize, value: bool) {
         assert!(index < STATE_LEN, "STATE_LEN is too small");
-        let idx = index / STATE_DATA_BITS;
-        // `STATE_DATA_BITS - 1 - ` fixes ordering
-        let bit = STATE_DATA_BITS - 1 - (index % STATE_DATA_BITS);
-
-        if value {
-            self.0[idx] |= 1 << bit;
-        } else {
-            self.0[idx] &= !(1 << bit);
-        }
+        self.0.set(index, value);
     }
 }
 
@@ -1067,18 +1069,19 @@ fn interpret(
     max_depth: Option<usize>,
     compress_traces: TraceCompression,
     print_timing: bool,
+    context: &Context,
 ) -> InterpreterResult {
     // States we have seen so far.
-    let mut seen: HashSet<BoundedState> = program.inits.iter().cloned().collect();
-
+    let mut seen = IsoStateSet::new(context);
     // The BFS queue, i.e., states on the frontier that need to be explored.
     // The queue is always a subset of seen.
-    let mut queue: VecDeque<Trace> = program
-        .inits
-        .iter()
-        .cloned()
-        .map(|state| Trace::new(state, compress_traces))
-        .collect();
+    let mut queue: VecDeque<Trace> = VecDeque::new();
+
+    for init in &program.inits {
+        if seen.insert(init) {
+            queue.push_back(Trace::new(*init, compress_traces));
+        }
+    }
 
     let mut transitions = Transitions::new();
     for tr in &program.trs {
@@ -1102,7 +1105,7 @@ fn interpret(
             println!(
                 "considering new depth: {current_depth}. \
                  queue length is {}. seen {} unique states.",
-                queue.len(),
+                queue.len() + 1, // include current state
                 seen.len()
             );
         }
@@ -1120,17 +1123,7 @@ fn interpret(
                 tr.updates
                     .iter()
                     .for_each(|update| next.set(update.index, update.formula.evaluate(state)));
-                if !seen.contains(&next) {
-                    seen.insert(next);
-                    if seen.len() % 1_000_000 == 0 {
-                        let elapsed = start_time.elapsed().as_secs_f64();
-                        println!(
-                            "progress report: ({elapsed:0.1}s since start) considering depth {current_depth}. \
-                             queue length is {}. visited {} states.",
-                            queue.len(),
-                            seen.len()
-                        );
-                    }
+                if seen.insert(&next) {
                     let mut trace = trace.clone();
                     trace.push(next);
                     queue.push_back(trace);
@@ -1208,6 +1201,242 @@ impl<'a> Transitions<'a> {
     }
 }
 
+/// Can answer the question "have I seen a state that is isomorphic to this one before"?
+struct IsoStateSet<'a> {
+    context: &'a Context<'a>,
+    data: HashMap<Fingerprint, Vec<(BoundedState, Partition)>>,
+}
+
+impl<'a> IsoStateSet<'a> {
+    fn new(context: &'a Context) -> IsoStateSet<'a> {
+        IsoStateSet {
+            context,
+            data: Default::default(),
+        }
+    }
+
+    fn len(&self) -> usize {
+        self.data.values().map(Vec::len).sum()
+    }
+
+    // true if insertion was successful
+    // false if element was already present
+    fn insert(&mut self, x: &BoundedState) -> bool {
+        let (fingerprint, xp) = self.fingerprint(x);
+        if let Some(vec) = self.data.get_mut(&fingerprint) {
+            if vec
+                .iter()
+                .any(|(y, yp)| is_isomorphic(self.context, x, &xp, y, yp))
+            {
+                false
+            } else {
+                vec.push((*x, xp));
+                true
+            }
+        } else {
+            self.data.insert(fingerprint.clone(), vec![(*x, xp)]);
+            true
+        }
+    }
+
+    fn fingerprint(&self, state: &BoundedState) -> (Fingerprint, Partition) {
+        let mut previous: HashMap<(&str, usize), usize> = self
+            .context
+            .signature
+            .sorts
+            .iter()
+            .enumerate()
+            .flat_map(|(i, s)| (0..self.context.universe[s]).map(move |e| ((s.as_str(), e), i)))
+            .collect();
+
+        for _ in 0..self.context.universe.values().sum() {
+            use std::collections::BTreeMap;
+            let mut current: HashMap<(&str, usize), BTreeMap<(&str, usize, Vec<Label>), usize>> =
+                previous.keys().map(|k| (*k, Default::default())).collect();
+
+            for ((name, elements), index) in &self.context.indices {
+                if state.get(*index) {
+                    let relation = self.context.signature.relation_decl(name);
+
+                    let labels: Vec<_> = (0..elements.len())
+                        .map(|i| match (&relation.args[i], elements[i]) {
+                            (Sort::Bool, 0) => Label::False,
+                            (Sort::Bool, 1) => Label::True,
+                            (Sort::Bool, _) => unreachable!(),
+                            (Sort::Uninterpreted(s), e) => Label::Other(previous[&(s.as_str(), e)]),
+                        })
+                        .collect();
+
+                    for (i, element) in elements.iter().enumerate() {
+                        if let Sort::Uninterpreted(s) = &relation.args[i] {
+                            *current
+                                .get_mut(&(s, *element))
+                                .unwrap()
+                                .entry((*name, i, labels.clone()))
+                                .or_insert(0) += 1;
+                        }
+                    }
+                }
+            }
+
+            let values_to_indices: HashMap<_, usize> = current
+                .values()
+                .cloned()
+                .sorted()
+                .unique()
+                .enumerate()
+                .map(|(i, x)| (x, i))
+                .collect();
+
+            previous = current
+                .into_iter()
+                .map(|(k, v)| (k, values_to_indices[&v]))
+                .collect();
+        }
+
+        let fingerprint: Vec<_> = previous
+            .iter()
+            .map(|((k, _), v)| (k.to_string(), *v))
+            .sorted()
+            .collect();
+
+        let mut classes: HashMap<&str, HashMap<usize, Vec<usize>>> = Default::default();
+        for ((s, e), l) in &previous {
+            classes
+                .entry(s)
+                .or_default()
+                .entry(*l)
+                .or_default()
+                .push(*e);
+        }
+
+        let partition: HashMap<_, Vec<_>> = classes
+            .into_iter()
+            .map(|(k, v)| {
+                (
+                    k.to_string(),
+                    v.into_iter().sorted().map(|(_, v)| v).collect(),
+                )
+            })
+            .collect();
+
+        (fingerprint, partition)
+    }
+}
+
+type Fingerprint = Vec<(String, usize)>;
+type Partition = HashMap<String, Vec<Vec<usize>>>;
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
+enum Label {
+    True,
+    False,
+    Other(usize),
+}
+
+fn is_isomorphic(
+    context: &Context,
+    x: &BoundedState,
+    px: &Partition,
+    y: &BoundedState,
+    py: &Partition,
+) -> bool {
+    if x == y {
+        return true;
+    }
+
+    assert_eq!(px.len(), py.len());
+
+    let permutations: Vec<Vec<Vec<usize>>> = px
+        .iter()
+        .sorted()
+        .zip(py.iter().sorted())
+        // the permutations are maps from old to new element values
+        .map(|((sx, vx), (sy, vy))| {
+            assert_eq!(sx, sy);
+            vx.iter()
+                .cloned()
+                .map(|v| {
+                    let l = v.len();
+                    v.into_iter().permutations(l)
+                })
+                .multi_cartesian_product_fixed()
+                .map(|permutation| {
+                    let mut func = vec![0; context.universe[sx]];
+                    assert_eq!(
+                        permutation.iter().map(|v| v.len()).sum::<usize>(),
+                        vy.iter().map(|v| v.len()).sum::<usize>()
+                    );
+                    assert_eq!(permutation.len(), vy.len());
+                    permutation
+                        .iter()
+                        .flatten()
+                        .zip(vy.iter().flatten())
+                        .for_each(|(ax, ay)| func[*ax] = *ay);
+                    func
+                })
+                .collect()
+        })
+        .collect();
+
+    let orderings: Vec<Vec<(usize, usize)>> = permutations
+        .into_iter()
+        // get all combinations of different ways to permute values
+        .multi_cartesian_product_fixed()
+        // reattach sort names onto each ordering
+        .map(|ordering| {
+            assert_eq!(context.signature.sorts.len(), ordering.len());
+            context
+                .signature
+                .sorts
+                .iter()
+                .map(|s| s.as_str())
+                .zip(ordering)
+                .collect()
+        })
+        // convert permutations to copy instructions
+        .map(|permutation: HashMap<&str, Vec<usize>>| {
+            context
+                .indices
+                .iter()
+                .map(|((name, elements), i)| {
+                    let relation = context.signature.relation_decl(name);
+                    assert_eq!(relation.args.len(), elements.len());
+                    // map each old element to a new element
+                    let mut new_elements = elements.clone();
+                    for i in 0..new_elements.len() {
+                        let x = elements[i];
+                        new_elements[i] = match &relation.args[i] {
+                            Sort::Uninterpreted(s) => permutation[s.as_str()][x],
+                            Sort::Bool => x,
+                        };
+                    }
+                    // look up the index to precompute the dst index
+                    (*i, context.indices[&(relation.name.as_str(), new_elements)])
+                })
+                .filter(|(i, j)| i != j)
+                .collect()
+        })
+        .collect();
+
+    'outer: for ordering in &orderings {
+        let mut new_state = *x;
+        for (src, dst) in ordering {
+            let x_bit = x.get(*src);
+            let y_bit = y.get(*dst);
+            if x_bit != y_bit {
+                continue 'outer;
+            }
+            new_state.set(*dst, x_bit);
+        }
+        if new_state == *y {
+            return true;
+        }
+    }
+
+    false
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -1277,12 +1506,6 @@ mod tests {
         assert!(!s.get(2));
         assert!(!s.get(3));
 
-        let mut a = BoundedState::ZERO;
-        let mut b = BoundedState::ZERO;
-        a.0[1] = 1; // [0, 1, 0, 0, ...]
-        b.0[0] = 1; // [1, 0, 0, 0, ...]
-        assert!(a < b);
-
         assert!(state([0]) < state([1]));
         assert!(state([0, 1, 0, 1]) < state([1, 0, 1, 0]));
         assert!(state([0, 1, 0, 0]) < state([0, 1, 0, 1]));
@@ -1292,6 +1515,18 @@ mod tests {
 
     #[test]
     fn checker_set_basic() {
+        let signature = Signature {
+            sorts: vec![],
+            relations: vec![RelationDecl {
+                args: vec![],
+                sort: Sort::Bool,
+                name: "r".to_string(),
+                mutable: true,
+            }],
+        };
+        let universe = std::collections::HashMap::new();
+        let context = Context::new(&signature, &universe);
+
         let program = BoundedProgram {
             inits: vec![state([0])],
             trs: vec![
@@ -1309,8 +1544,8 @@ mod tests {
                 value: false,
             }),
         };
-        let result0 = interpret(&program, Some(0), TraceCompression::No, false);
-        let result1 = interpret(&program, Some(1), TraceCompression::No, false);
+        let result0 = interpret(&program, Some(0), TraceCompression::No, false, &context);
+        let result1 = interpret(&program, Some(1), TraceCompression::No, false, &context);
         assert_eq!(result0, InterpreterResult::Unknown);
         let mut expected1 = Trace::new(state([0]), TraceCompression::No);
         expected1.push(state([1]));
@@ -1319,6 +1554,38 @@ mod tests {
 
     #[test]
     fn checker_set_cycle() {
+        let signature = Signature {
+            sorts: vec![],
+            relations: vec![
+                RelationDecl {
+                    args: vec![],
+                    sort: Sort::Bool,
+                    name: "0".to_string(),
+                    mutable: true,
+                },
+                RelationDecl {
+                    args: vec![],
+                    sort: Sort::Bool,
+                    name: "1".to_string(),
+                    mutable: true,
+                },
+                RelationDecl {
+                    args: vec![],
+                    sort: Sort::Bool,
+                    name: "2".to_string(),
+                    mutable: true,
+                },
+                RelationDecl {
+                    args: vec![],
+                    sort: Sort::Bool,
+                    name: "3".to_string(),
+                    mutable: true,
+                },
+            ],
+        };
+        let universe = std::collections::HashMap::new();
+        let context = Context::new(&signature, &universe);
+
         let program = BoundedProgram {
             inits: vec![state([1, 0, 0, 0])],
             trs: vec![
@@ -1392,11 +1659,11 @@ mod tests {
                 value: false,
             }),
         };
-        let result1 = interpret(&program, Some(0), TraceCompression::No, false);
-        let result2 = interpret(&program, Some(1), TraceCompression::No, false);
-        let result3 = interpret(&program, Some(2), TraceCompression::No, false);
-        let result4 = interpret(&program, Some(3), TraceCompression::No, false);
-        let result5 = interpret(&program, Some(4), TraceCompression::No, false);
+        let result1 = interpret(&program, Some(0), TraceCompression::No, false, &context);
+        let result2 = interpret(&program, Some(1), TraceCompression::No, false, &context);
+        let result3 = interpret(&program, Some(2), TraceCompression::No, false, &context);
+        let result4 = interpret(&program, Some(3), TraceCompression::No, false, &context);
+        let result5 = interpret(&program, Some(4), TraceCompression::No, false, &context);
         assert_eq!(result1, InterpreterResult::Unknown);
         assert_eq!(result2, InterpreterResult::Unknown);
         assert_eq!(result3, InterpreterResult::Unknown);
@@ -1507,7 +1774,7 @@ mod tests {
             target.trs.iter().sorted().collect::<Vec<_>>(),
         );
 
-        let output = interpret(&target, None, TraceCompression::No, false);
+        let output = interpret(&target, None, TraceCompression::No, false, &context);
         assert_eq!(output, InterpreterResult::Convergence);
 
         Ok(())
@@ -1520,16 +1787,16 @@ mod tests {
         let mut m = fly::parser::parse(source).unwrap();
         sort_check_and_infer(&mut m).unwrap();
         let universe = std::collections::HashMap::from([("node".to_string(), 2)]);
-        let (target, _) = translate(&m, &universe, false)?;
+        let (target, context) = translate(&m, &universe, false)?;
 
-        let bug = interpret(&target, Some(12), TraceCompression::No, false);
+        let bug = interpret(&target, Some(12), TraceCompression::No, false, &context);
         if let InterpreterResult::Counterexample(trace) = &bug {
             assert_eq!(trace.depth(), 12);
         } else {
             assert!(matches!(bug, InterpreterResult::Counterexample(_)));
         }
 
-        let too_short = interpret(&target, Some(11), TraceCompression::No, false);
+        let too_short = interpret(&target, Some(11), TraceCompression::No, false, &context);
         assert_eq!(too_short, InterpreterResult::Unknown);
 
         Ok(())
@@ -1582,4 +1849,104 @@ assume always forall a:x. ((g'(a) <-> f(a)) & (f'(a) <-> f(a)))
         assert_eq!(1, target.trs.len());
         Ok(())
     }
+
+    #[test]
+    fn checker_set_isostateset_correctness() {
+        let source = "
+sort s
+immutable f(s): bool
+        ";
+        let m = fly::parser::parse(source).unwrap();
+        let universe = std::collections::HashMap::from([("s".to_string(), 2)]);
+        let context = Context::new(&m.signature, &universe);
+        let mut set = IsoStateSet::new(&context);
+
+        assert!(set.insert(&state([0, 0])));
+        assert!(!set.insert(&state([0, 0])));
+        assert!(set.insert(&state([0, 1])));
+        assert!(!set.insert(&state([1, 0])));
+        assert!(set.insert(&state([1, 1])));
+
+        let source = "
+sort a
+sort b
+immutable f(a, b): bool
+        ";
+        let m = fly::parser::parse(source).unwrap();
+        let universe =
+            std::collections::HashMap::from([("a".to_string(), 3), ("b".to_string(), 3)]);
+        let context = Context::new(&m.signature, &universe);
+        let mut set = IsoStateSet::new(&context);
+
+        // b: 0 -> 2, 2 -> 1, 1 -> 0
+        assert!(set.insert(&state([1, 1, 1, 0, 0, 1, 0, 1, 1])));
+        assert!(!set.insert(&state([1, 1, 1, 0, 1, 0, 1, 1, 0])));
+
+        let source = "
+sort s
+sort t
+immutable f(s, t, s): bool
+        ";
+        let m = fly::parser::parse(source).unwrap();
+        let universe =
+            std::collections::HashMap::from([("s".to_string(), 3), ("t".to_string(), 2)]);
+        let context = Context::new(&m.signature, &universe);
+        let mut set = IsoStateSet::new(&context);
+        let state = |vec: Vec<(usize, usize, usize)>| -> BoundedState {
+            let mut out = BoundedState::ZERO;
+            for (x, y, z) in vec {
+                out.set(context.indices[&("f", vec![x, y, z])], true);
+            }
+            out
+        };
+
+        assert!(set.insert(&state(vec![(0, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 1)])));
+        assert!(!set.insert(&state(vec![(2, 0, 2)])));
+        assert!(!set.insert(&state(vec![(0, 1, 0)])));
+        assert!(!set.insert(&state(vec![(1, 1, 1)])));
+        assert!(!set.insert(&state(vec![(2, 1, 2)])));
+
+        assert!(set.insert(&state(vec![(1, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 0)])));
+        assert!(!set.insert(&state(vec![(2, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 1, 0)])));
+        assert!(!set.insert(&state(vec![(0, 1, 1)])));
+
+        assert!(set.insert(&state(vec![(0, 0, 0), (0, 1, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 1), (1, 1, 1)])));
+        assert!(set.insert(&state(vec![(0, 0, 1), (0, 1, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 0), (1, 1, 1)])));
+        assert!(!set.insert(&state(vec![(0, 1, 1), (0, 0, 0)])));
+
+        let source = "
+sort s
+immutable f(s, bool, s): bool
+        ";
+        let m = fly::parser::parse(source).unwrap();
+        let universe = std::collections::HashMap::from([("s".to_string(), 3)]);
+        let context = Context::new(&m.signature, &universe);
+        let mut set = IsoStateSet::new(&context);
+        let state = |vec: Vec<(usize, usize, usize)>| -> BoundedState {
+            let mut out = BoundedState::ZERO;
+            for (x, y, z) in vec {
+                out.set(context.indices[&("f", vec![x, y, z])], true);
+            }
+            out
+        };
+
+        assert!(set.insert(&state(vec![(0, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 1)])));
+        assert!(!set.insert(&state(vec![(2, 0, 2)])));
+        assert!(set.insert(&state(vec![(0, 1, 0)])));
+        assert!(!set.insert(&state(vec![(1, 1, 1)])));
+        assert!(!set.insert(&state(vec![(2, 1, 2)])));
+
+        assert!(set.insert(&state(vec![(1, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 0)])));
+        assert!(!set.insert(&state(vec![(2, 0, 0)])));
+
+        assert!(set.insert(&state(vec![(1, 1, 0)])));
+        assert!(!set.insert(&state(vec![(0, 1, 1)])));
+    }
 }
diff --git a/temporal-verifier/tests/examples/snapshots/lockserver_buggy.fly.2.snap b/temporal-verifier/tests/examples/snapshots/lockserver_buggy.fly.2.snap
index 3151360e..36261e8b 100644
--- a/temporal-verifier/tests/examples/snapshots/lockserver_buggy.fly.2.snap
+++ b/temporal-verifier/tests/examples/snapshots/lockserver_buggy.fly.2.snap
@@ -7,18 +7,18 @@ starting translation...
 enumerating 1 initial states
 enumerating 15 transitions
 starting search from depth 0. there are 1 initial states in the queue.
-considering new depth: 1. queue length is 2. seen 4 unique states.
-considering new depth: 2. queue length is 5. seen 10 unique states.
-considering new depth: 3. queue length is 12. seen 23 unique states.
-considering new depth: 4. queue length is 20. seen 44 unique states.
-considering new depth: 5. queue length is 23. seen 68 unique states.
-considering new depth: 6. queue length is 20. seen 89 unique states.
-considering new depth: 7. queue length is 20. seen 110 unique states.
-considering new depth: 8. queue length is 47. seen 158 unique states.
-considering new depth: 9. queue length is 92. seen 251 unique states.
-considering new depth: 10. queue length is 110. seen 362 unique states.
-considering new depth: 11. queue length is 125. seen 488 unique states.
-considering new depth: 12. queue length is 200. seen 689 unique states.
+considering new depth: 1. queue length is 1. seen 4 unique states.
+considering new depth: 2. queue length is 2. seen 10 unique states.
+considering new depth: 3. queue length is 4. seen 23 unique states.
+considering new depth: 4. queue length is 5. seen 44 unique states.
+considering new depth: 5. queue length is 6. seen 68 unique states.
+considering new depth: 6. queue length is 5. seen 89 unique states.
+considering new depth: 7. queue length is 5. seen 110 unique states.
+considering new depth: 8. queue length is 10. seen 158 unique states.
+considering new depth: 9. queue length is 18. seen 251 unique states.
+considering new depth: 10. queue length is 22. seen 362 unique states.
+considering new depth: 11. queue length is 25. seen 488 unique states.
+considering new depth: 12. queue length is 38. seen 689 unique states.
 found counterexample:
 state 0:
 lock_msg(@node_0) = false