diff --git a/src/logic.py b/src/logic.py
index 03153c8..f68aa85 100755
--- a/src/logic.py
+++ b/src/logic.py
@@ -388,7 +388,13 @@ def _read_first_order_structure(struct: FirstOrderStructure) -> Tuple[
                 e = e if ans else syntax.Not(e)
                 rels[R].append(e)
         for C, c in struct.const_interps.items():
-            e = syntax.Eq(syntax.Id(C.name), syntax.Id(c))
+            # There are two cases, c is either another Id or a constant
+            # Constants are produced as dicts of the form {(): bool(ans)}
+            # in translator.py:Z3Translator:_old_model_to_trace
+            if isinstance(c, dict) and () in c:
+                e = syntax.Eq(syntax.Id(C.name), syntax.Bool(c[()]))
+            else:
+                e = syntax.Eq(syntax.Id(C.name), syntax.Id(c))
             consts[C] = e
         for F, fl in struct.func_interps.items():
             funcs[F] = []
@@ -435,8 +441,14 @@ def const_subst(self) -> Dict[syntax.Id, syntax.Id]:
         ans = {}
         for c, e in self.consts.items():
             assert isinstance(e, syntax.BinaryExpr) and e.op == 'EQUAL' and \
-                isinstance(e.arg1, syntax.Id) and isinstance(e.arg2, syntax.Id)
-            ans[e.arg2] = e.arg1
+                isinstance(e.arg1, syntax.Id)
+            if isinstance(e.arg2, syntax.Id):
+                ans[e.arg2] = e.arg1
+            else:
+                # Sometimes we get a boolean on the RHS of the equality,
+                # and there is no need to substitute it.
+                # TODO: should we then do ans[e.arg1] = e.arg2?
+                pass
         return ans
 
     def conjuncts(self) -> Iterable[Tuple[_RelevantDecl, int, Expr]]: