diff --git a/bounded/src/bdd.rs b/bounded/src/bdd.rs
index be8c9305..1cbc7c07 100644
--- a/bounded/src/bdd.rs
+++ b/bounded/src/bdd.rs
@@ -294,12 +294,12 @@ fn check_internal<'a>(
 
     for relation in &module.signature.relations {
         if relation.sort != Sort::Bool {
-            todo!("non-bool relations")
+            panic!("non-bool relations in checker (use Module::convert_non_bool_relations)")
         }
     }
 
     if !module.defs.is_empty() {
-        todo!("definitions are not supported yet");
+        panic!("definitions in checker (use Module::inline_defs)")
     }
 
     let d = extract(module).map_err(CheckerError::ExtractionError)?;
diff --git a/bounded/src/sat.rs b/bounded/src/sat.rs
index 7751e125..209fdf1b 100644
--- a/bounded/src/sat.rs
+++ b/bounded/src/sat.rs
@@ -168,12 +168,12 @@ pub fn check(
 
     for relation in &module.signature.relations {
         if relation.sort != Sort::Bool {
-            todo!("non-bool relations")
+            panic!("non-bool relations in checker (use Module::convert_non_bool_relations)")
         }
     }
 
     if !module.defs.is_empty() {
-        todo!("definitions are not supported yet");
+        panic!("definitions in checker (use Module::inline_defs)")
     }
 
     let d = extract(module).map_err(CheckerError::ExtractionError)?;
diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index b9f47b97..1fe0134a 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -563,7 +563,7 @@ fn translate<'a>(
 ) -> Result<(BoundedProgram, Indices<'a>), TranslationError> {
     for relation in &module.signature.relations {
         if relation.sort != Sort::Bool {
-            todo!("non-bool relations")
+            panic!("non-bool relations in checker (use Module::convert_non_bool_relations)")
         }
     }
 
@@ -579,7 +579,7 @@ fn translate<'a>(
     }
 
     if !module.defs.is_empty() {
-        todo!("definitions are not supported yet");
+        panic!("definitions in checker (use Module::inline_defs)")
     }
 
     let d = extract(module).map_err(TranslationError::ExtractionError)?;
diff --git a/bounded/src/smt.rs b/bounded/src/smt.rs
index 82458b47..92890719 100644
--- a/bounded/src/smt.rs
+++ b/bounded/src/smt.rs
@@ -37,7 +37,7 @@ pub fn check(
     print_timing: bool,
 ) -> Result<CheckerAnswer, CheckerError> {
     if !module.defs.is_empty() {
-        todo!("definitions are not supported yet");
+        panic!("definitions are not supported yet");
     }
 
     let d = extract(module).map_err(CheckerError::ExtractionError)?;
diff --git a/fly/src/lib.rs b/fly/src/lib.rs
index e3b982d6..ca5ff691 100644
--- a/fly/src/lib.rs
+++ b/fly/src/lib.rs
@@ -18,6 +18,7 @@ pub mod defs;
 pub mod ouritertools;
 pub mod parser;
 pub mod printer;
+pub mod rets;
 pub mod semantics;
 pub mod sorts;
 pub mod syntax;
diff --git a/fly/src/rets.rs b/fly/src/rets.rs
new file mode 100644
index 00000000..91ddf73e
--- /dev/null
+++ b/fly/src/rets.rs
@@ -0,0 +1,381 @@
+// Copyright 2022-2023 VMware, Inc.
+// SPDX-License-Identifier: BSD-2-Clause
+
+//! Utility to convert all non-boolean-returning relations in a Module to boolean-returning ones.
+
+use crate::{semantics::*, syntax::*};
+
+impl Module {
+    /// Converts all non-boolean-returning relations to boolean-returning ones
+    /// by adding an extra argument and axioms.
+    pub fn convert_non_bool_relations(&mut self) -> Box<dyn Fn(&Model) -> Model> {
+        let old_signature = self.signature.clone();
+        let changed: Vec<_> = old_signature
+            .relations
+            .iter()
+            .filter(|r| r.sort != Sort::Bool)
+            .cloned()
+            .collect();
+
+        let mut axioms = vec![];
+        for relation in &mut self.signature.relations {
+            if relation.sort != Sort::Bool {
+                let binders: Vec<Binder> = relation
+                    .args
+                    .iter()
+                    .chain([&relation.sort, &relation.sort])
+                    .enumerate()
+                    .map(|(i, sort)| Binder {
+                        sort: sort.clone(),
+                        name: format!("__{i}"),
+                    })
+                    .collect();
+                let other_args = &binders[0..relation.args.len()];
+                let new_arg_twice = &binders[relation.args.len()..];
+                let all_args_new: Vec<_> = binders[0..=relation.args.len()]
+                    .iter()
+                    .map(|b| Term::Id(b.name.clone()))
+                    .collect();
+                let mut all_args_new_alt = all_args_new.clone();
+                *all_args_new_alt.last_mut().unwrap() =
+                    Term::Id(binders.last().unwrap().name.clone());
+
+                let at_least_one = Term::exists(
+                    [binders[relation.args.len()].clone()],
+                    Term::App(relation.name.clone(), 0, all_args_new.clone()),
+                );
+                let at_most_one = Term::forall(
+                    new_arg_twice.iter().cloned(),
+                    Term::implies(
+                        Term::and([
+                            Term::App(relation.name.clone(), 0, all_args_new),
+                            Term::App(relation.name.clone(), 0, all_args_new_alt),
+                        ]),
+                        Term::equals(
+                            Term::Id(new_arg_twice[0].name.clone()),
+                            Term::Id(new_arg_twice[1].name.clone()),
+                        ),
+                    ),
+                );
+
+                let at_least_one = match relation.args.len() {
+                    0 => at_least_one,
+                    _ => Term::forall(other_args.iter().cloned(), at_least_one),
+                };
+                let at_most_one = match relation.args.len() {
+                    0 => at_most_one,
+                    _ => Term::forall(other_args.iter().cloned(), at_most_one),
+                };
+
+                axioms.push(ThmStmt::Assume(Term::UnaryOp(
+                    UOp::Always,
+                    Box::new(at_least_one),
+                )));
+                axioms.push(ThmStmt::Assume(Term::UnaryOp(
+                    UOp::Always,
+                    Box::new(at_most_one),
+                )));
+
+                relation.args.push(relation.sort.clone());
+                relation.sort = Sort::Bool;
+            }
+        }
+
+        let mut name = 0;
+        let mut go = |term: &mut Term| {
+            let to_quantify = fix_term(term, &changed, &mut name);
+            assert!(to_quantify.is_empty(), "{to_quantify:?}");
+        };
+        for statement in &mut self.statements {
+            match statement {
+                ThmStmt::Assume(term) => go(term),
+                ThmStmt::Assert(Proof { assert, invariants }) => {
+                    go(&mut assert.x);
+                    for invariant in invariants {
+                        go(&mut invariant.x);
+                    }
+                }
+            }
+        }
+
+        self.statements.splice(0..0, axioms);
+
+        Box::new(move |model| {
+            Model::new(
+                &old_signature,
+                &model.universe,
+                old_signature
+                    .relations
+                    .iter()
+                    .map(|r| {
+                        let interp = &model.interp[old_signature.relation_idx(&r.name)];
+                        if r.sort == Sort::Bool {
+                            return interp.clone();
+                        }
+
+                        let shape = r
+                            .args
+                            .iter()
+                            .map(|s| model.cardinality(s))
+                            .chain([model.cardinality(&r.sort)])
+                            .collect();
+                        let f = |elements: &[Element]| {
+                            for i in 0..model.cardinality(&r.sort) {
+                                let mut elements = elements.to_vec();
+                                elements.push(i);
+                                if interp.get(&elements) == 1 {
+                                    return i;
+                                }
+                            }
+                            unreachable!()
+                        };
+                        Interpretation::new(&shape, f)
+                    })
+                    .collect(),
+            )
+        })
+    }
+}
+
+#[derive(Debug)]
+struct ToBeQuantified {
+    name: String,
+    sort: Sort,
+    r: String,
+    p: usize,
+    xs: Vec<Term>,
+    primes: usize,
+}
+
+fn fix_term(term: &mut Term, changed: &[RelationDecl], name: &mut usize) -> Vec<ToBeQuantified> {
+    // wraps term with an exists quantifier
+    let quantify = |term: &mut Term, to_quantify: Vec<ToBeQuantified>| {
+        if !to_quantify.is_empty() {
+            let mut binders = vec![];
+            let mut clauses = vec![term.clone()];
+            for mut tbq in to_quantify.into_iter().rev() {
+                tbq.xs.push(Term::Id(tbq.name.clone()));
+                binders.insert(
+                    0,
+                    Binder {
+                        name: tbq.name,
+                        sort: tbq.sort,
+                    },
+                );
+                let mut clause = Term::App(tbq.r, tbq.p, tbq.xs);
+                for _ in 0..tbq.primes {
+                    clause = Term::UnaryOp(UOp::Prime, Box::new(clause));
+                }
+                clauses.insert(0, clause);
+            }
+            *term = Term::exists(binders, Term::and(clauses));
+        }
+    };
+
+    match term {
+        Term::Id(r) => {
+            let mut out = vec![];
+            if let Some(c) = changed.iter().find(|c| r == &c.name) {
+                *name += 1;
+                let name = format!("___{}", *name);
+                out.push(ToBeQuantified {
+                    name: name.clone(),
+                    sort: c.sort.clone(),
+                    r: r.to_string(),
+                    p: 0,
+                    xs: vec![],
+                    primes: 0,
+                });
+                *term = Term::Id(name);
+            }
+            out
+        }
+        Term::App(r, p, xs) => {
+            let mut out = vec![];
+            for x in &mut *xs {
+                out.extend(fix_term(x, changed, name));
+            }
+            if let Some(c) = changed.iter().find(|c| r == &c.name) {
+                *name += 1;
+                let name = format!("___{}", *name);
+                out.push(ToBeQuantified {
+                    name: name.clone(),
+                    sort: c.sort.clone(),
+                    r: r.to_string(),
+                    p: *p,
+                    xs: xs.to_vec(),
+                    primes: 0,
+                });
+                *term = Term::Id(name);
+            }
+            out
+        }
+        Term::UnaryOp(UOp::Always | UOp::Eventually, a) => {
+            let to_quantify = fix_term(a, changed, name);
+            quantify(a, to_quantify);
+            vec![]
+        }
+        Term::UnaryOp(UOp::Prime | UOp::Next, a) => fix_term(a, changed, name)
+            .into_iter()
+            .map(|tbq| ToBeQuantified {
+                primes: tbq.primes + 1,
+                ..tbq
+            })
+            .collect(),
+        Term::UnaryOp(UOp::Previous, _) => todo!(),
+        Term::UnaryOp(_, a) => fix_term(a, changed, name),
+        Term::BinOp(BinOp::Until | BinOp::Since, a, b) => {
+            let to_quantify = fix_term(a, changed, name);
+            quantify(a, to_quantify);
+            let to_quantify = fix_term(b, changed, name);
+            quantify(b, to_quantify);
+            vec![]
+        }
+        Term::BinOp(_, a, b) => {
+            let mut out = vec![];
+            out.extend(fix_term(a, changed, name));
+            out.extend(fix_term(b, changed, name));
+            out
+        }
+        Term::NAryOp(_, terms) => {
+            let mut out = vec![];
+            for term in terms {
+                out.extend(fix_term(term, changed, name));
+            }
+            out
+        }
+        Term::Ite { cond, then, else_ } => {
+            let mut out = vec![];
+            out.extend(fix_term(cond, changed, name));
+            out.extend(fix_term(then, changed, name));
+            out.extend(fix_term(else_, changed, name));
+            out
+        }
+        Term::Quantified { body, .. } => {
+            let to_quantify = fix_term(body, changed, name);
+            quantify(body, to_quantify);
+            vec![]
+        }
+        Term::Literal(_) => vec![],
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::{parser::parse, semantics::*};
+
+    #[test]
+    fn non_bool_relations_module_conversion_basic() {
+        let source1 = "
+sort s
+mutable f(s, bool): s
+
+assume always forall s:s. f(s, true) = s
+        ";
+        let source2 = "
+sort s
+mutable f(s, bool, s): bool
+
+assume always forall __0:s, __1: bool. exists __2:s. f(__0, __1, __2)
+assume always forall __0:s, __1: bool, __2:s, __3:s.
+    (f(__0, __1, __2) & f(__0, __1, __3)) -> (__2 = __3)
+
+assume always forall s:s. exists ___1:s. f(s, true, ___1) & ___1 = s
+        ";
+
+        let mut module1 = parse(source1).unwrap();
+        let _ = module1.convert_non_bool_relations();
+
+        let module2 = parse(source2).unwrap();
+
+        assert_eq!(module2, module1);
+    }
+
+    #[test]
+    fn non_bool_relations_module_conversion_primes() {
+        let source1 = "
+sort s
+mutable f(s): s
+
+assume always forall s:s. (f(s))' = s
+        ";
+        let source2 = "
+sort s
+mutable f(s, s): bool
+
+assume always forall __0:s. exists __1:s. f(__0, __1)
+assume always forall __0:s, __1:s, __2:s. (f(__0, __1) & f(__0, __2)) -> (__1 = __2)
+
+assume always forall s:s. exists ___1:s. (f(s, ___1))' & ___1' = s
+        ";
+
+        let mut module1 = parse(source1).unwrap();
+        let _ = module1.convert_non_bool_relations();
+
+        let module2 = parse(source2).unwrap();
+
+        assert_eq!(module2, module1);
+    }
+
+    #[test]
+    fn non_bool_relations_module_conversion_nested() {
+        let source1 = "
+sort s
+mutable f: s
+
+assume always forall s:s. f = s & (forall s:s. s=s)
+        ";
+        let source2 = "
+sort s
+mutable f(s): bool
+
+assume always exists __0:s. f(__0)
+assume always forall __0:s, __1:s. (f(__0) & f(__1)) -> (__0 = __1)
+
+assume always forall s:s. exists ___1:s. f(___1) & ___1 = s & forall s:s. s=s
+        ";
+
+        let mut module1 = parse(source1).unwrap();
+        let _ = module1.convert_non_bool_relations();
+
+        let module2 = parse(source2).unwrap();
+
+        assert_eq!(module2, module1);
+    }
+
+    #[test]
+    fn non_bool_relations_model_back_conversion() {
+        let source = "
+sort s
+
+mutable f(bool): s
+        ";
+        let mut module = parse(source).unwrap();
+
+        let model1 = Model::new(
+            &module.signature,
+            &vec![3],
+            vec![Interpretation::new(&vec![2, 3], |xs| {
+                if xs[0] == 0 {
+                    2
+                } else {
+                    0
+                }
+            })],
+        );
+
+        let back_convert_model = module.convert_non_bool_relations();
+        let model2 = Model::new(
+            &module.signature,
+            &vec![3],
+            vec![Interpretation::new(&vec![2, 3, 2], |xs| match xs {
+                [0, 2] | [1, 0] => 1,
+                _ => 0,
+            })],
+        );
+
+        let model3 = back_convert_model(&model2);
+
+        assert_eq!(model1, model3);
+    }
+}
diff --git a/fly/src/semantics.rs b/fly/src/semantics.rs
index feff240b..26b9a681 100644
--- a/fly/src/semantics.rs
+++ b/fly/src/semantics.rs
@@ -92,7 +92,8 @@ pub struct Model {
 }
 
 impl Model {
-    fn cardinality(&self, sort: &Sort) -> usize {
+    /// Get the cardinality using the universe from this model
+    pub fn cardinality(&self, sort: &Sort) -> usize {
         match sort {
             Sort::Bool => 2,
             _ => self.universe[self.signature.sort_idx(sort)],
@@ -111,8 +112,7 @@ impl Model {
                 &self.cardinality(&relation.sort),
             );
             for j in 0..relation.args.len() {
-                let k = self.signature.sort_idx(&relation.args[j]);
-                assert_eq!(interp.shape[j], self.universe[k]);
+                assert_eq!(self.cardinality(&relation.args[j]), interp.shape[j]);
             }
         }
     }
diff --git a/temporal-verifier/src/command.rs b/temporal-verifier/src/command.rs
index 51fdb273..b2fd54c3 100644
--- a/temporal-verifier/src/command.rs
+++ b/temporal-verifier/src/command.rs
@@ -568,6 +568,8 @@ impl App {
                 bounded,
                 compress_traces,
             } => {
+                m.inline_defs();
+                let back_convert_model = m.convert_non_bool_relations();
                 let univ = bounded.get_universe(&m.signature);
                 match bounded::set::check(
                     &m,
@@ -580,7 +582,7 @@ impl App {
                         println!("found counterexample:");
                         for (i, model) in models.iter().enumerate() {
                             println!("state {i}:");
-                            println!("{}", model.fmt());
+                            println!("{}", back_convert_model(model).fmt());
                         }
                     }
                     Ok(bounded::set::CheckerAnswer::Unknown) => {
@@ -599,6 +601,8 @@ impl App {
                 }
             }
             Command::SatCheck(bounded) => {
+                m.inline_defs();
+                let back_convert_model = m.convert_non_bool_relations();
                 let depth = match bounded.depth {
                     Some(depth) => depth,
                     None => {
@@ -612,7 +616,7 @@ impl App {
                         println!("found counterexample:");
                         for (i, model) in models.iter().enumerate() {
                             println!("state {i}:");
-                            println!("{}", model.fmt());
+                            println!("{}", back_convert_model(model).fmt());
                         }
                     }
                     Ok(bounded::sat::CheckerAnswer::Unknown) => {
@@ -622,6 +626,8 @@ impl App {
                 }
             }
             Command::BddCheck { bounded, reversed } => {
+                m.inline_defs();
+                let back_convert_model = m.convert_non_bool_relations();
                 let univ = bounded.get_universe(&m.signature);
                 let check = match reversed {
                     false => bounded::bdd::check,
@@ -637,7 +643,7 @@ impl App {
                         println!("found counterexample:");
                         for (i, model) in models.iter().enumerate() {
                             println!("state {i}:");
-                            println!("{}", model.fmt());
+                            println!("{}", back_convert_model(model).fmt());
                         }
                     }
                     Ok(bounded::bdd::CheckerAnswer::Unknown) => {
@@ -656,6 +662,7 @@ impl App {
                 }
             }
             Command::SmtCheck { bounded, solver } => {
+                m.inline_defs();
                 let depth = match bounded.depth {
                     Some(depth) => depth,
                     None => {