diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 1666207c..b05a9600 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -13,8 +13,16 @@ jobs:
     - uses: avsm/setup-ocaml@master
       with:
         ocaml-version: ${{ matrix.ocaml-version }}
+    - name: cache opam
+      id: cache-opam
+      uses: actions/cache@v2
+      with:
+        path: _opam
+        key: opam-${{matrix.operating-system}}-${{matrix.ocaml-version}}
     - run: opam pin -n .
     - run: opam depext -yt sidekick-bin
+      if: steps.cache-opam.outputs.cache-hit != 'true'
     - run: opam install -t . --deps-only
+      if: steps.cache-opam.outputs.cache-hit != 'true'
     - run: opam exec -- dune build
     - run: opam exec -- dune runtest
diff --git a/Makefile b/Makefile
index be7fc5f6..aba219b0 100644
--- a/Makefile
+++ b/Makefile
@@ -44,6 +44,9 @@ $(TESTTOOL)-smt-QF_DT: snapshots
 $(TESTTOOL)-smt-QF_LRA: snapshots
 	$(TESTTOOL) run $(TESTOPTS) \
 	  --csv snapshots/smt-QF_LRA-$(DATE).csv --task sidekick-smt-nodir tests/QF_LRA
+$(TESTTOOL)-smt-QF_UFLRA: snapshots
+	$(TESTTOOL) run $(TESTOPTS) \
+	  --csv snapshots/smt-QF_UFLRA-$(DATE).csv --task sidekick-smt-nodir tests/QF_UFLRA
 
 install: build-install
 	@dune install
diff --git a/dune-project b/dune-project
index 00d8427e..89f5a4d0 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,2 @@
 (lang dune 1.6)
 (using menhir 1.0)
-(using fmt 1.1)
diff --git a/sidekick-bin.opam b/sidekick-bin.opam
index 83de23dd..becbc5e9 100644
--- a/sidekick-bin.opam
+++ b/sidekick-bin.opam
@@ -15,10 +15,10 @@ depends: [
   "containers" { >= "3.0" & < "4.0" }
   "iter"
   "zarith"
-  "smtlib-utils" { >= "0.1" & < "0.2" }
+  "smtlib-utils" { >= "0.1" & < "0.3" }
   "sidekick" { = version }
   "menhir"
-  "msat" { >= "0.8" < "0.9" }
+  "mtime"
   "ocaml" { >= "4.03" }
 ]
 tags: [ "sat" "smt" ]
diff --git a/sidekick.opam b/sidekick.opam
index bd4cf5ed..59f48965 100644
--- a/sidekick.opam
+++ b/sidekick.opam
@@ -14,7 +14,7 @@ depends: [
   "dune" { >= "1.1" }
   "containers" { >= "3.0" & < "4.0" }
   "iter" { >= "1.0" & < "2.0" }
-  "msat" { >= "0.8.3" < "0.9" }
+  "msat" { >= "0.9" < "0.10" }
   "ocaml" { >= "4.03" }
   "alcotest" {with-test}
 ]
diff --git a/src/arith/base-term/Base_types.ml b/src/arith/base-term/Base_types.ml
index 4d0cab95..affedece 100644
--- a/src/arith/base-term/Base_types.ml
+++ b/src/arith/base-term/Base_types.ml
@@ -914,6 +914,8 @@ end = struct
     | Eq (a,b) -> C.Eq (a, b)
     | Not u -> C.Not u
     | Ite (a,b,c) -> C.If (a,b,c)
+    | LRA (LRA_pred (Eq, a, b)) ->
+      C.Eq (a,b) (* need congruence closure on this one, for theory combination *)
     | LRA _ -> C.Opaque t (* no congruence here *)
 
   module As_key = struct
diff --git a/src/arith/lra/linear_expr_intf.ml b/src/arith/lra/linear_expr_intf.ml
index 8a73c37b..14b7b619 100644
--- a/src/arith/lra/linear_expr_intf.ml
+++ b/src/arith/lra/linear_expr_intf.ml
@@ -134,7 +134,7 @@ module type S = sig
       to coefficients. This allows for very fast computations.
   *)
   module Comb : sig
-    type t = private C.t Var_map.t
+    type t
     (** The type of linear combinations. *)
 
     val compare : t -> t -> int
diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml
index 6c870f04..8d1d823f 100644
--- a/src/arith/lra/sidekick_arith_lra.ml
+++ b/src/arith/lra/sidekick_arith_lra.ml
@@ -43,6 +43,9 @@ module type ARG = sig
 
   val ty_lra : S.T.Term.state -> ty
 
+  val has_ty_real : term -> bool
+  (** Does this term have the type [Real] *)
+
   module Gensym : sig
     type t
 
@@ -73,18 +76,37 @@ module Make(A : ARG) : S with module A = A = struct
   module T = A.S.T.Term
   module Lit = A.S.Solver_internal.Lit
   module SI = A.S.Solver_internal
+  module N = A.S.Solver_internal.CC.N
+
+  module Tag = struct
+    type t =
+      | By_def
+      | Lit of Lit.t
+      | CC_eq of N.t * N.t
+
+    let pp out = function
+      | By_def -> Fmt.string out "<bydef>"
+      | Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l
+      | CC_eq (n1,n2) -> Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" N.pp n1 N.pp n2
+
+    let to_lits si = function
+      | By_def -> []
+      | Lit l -> [l]
+      | CC_eq (n1,n2) ->
+        SI.CC.explain_eq (SI.cc si) n1 n2
+  end
 
   module SimpVar
     : Linear_expr.VAR_GEN
       with type t = A.term
        and type Fresh.t = A.Gensym.t
-       and type lit = Lit.t
+       and type lit = Tag.t
   = struct
     type t = A.term
     let pp = A.S.T.Term.pp
     let compare = A.S.T.Term.compare
-    type lit = Lit.t
-    let pp_lit = Lit.pp
+    type lit = Tag.t
+    let pp_lit = Tag.pp
     module Fresh = struct
       type t = A.Gensym.t
       let copy = A.Gensym.copy
@@ -101,14 +123,17 @@ module Make(A : ARG) : S with module A = A = struct
   module LE = SimpSolver.L.Expr
   module LConstr = SimpSolver.L.Constr
 
+  type proxy = T.t
   type state = {
     tst: T.state;
     simps: T.t T.Tbl.t; (* cache *)
     gensym: A.Gensym.t;
     neq_encoded: unit T.Tbl.t;
     (* if [a != b] asserted and not in this table, add clause [a = b \/ a<b \/ a>b] *)
-    mutable t_defs: (T.t * LE.t) list; (* term definitions *)
-    pred_defs: (pred * LE.t * LE.t) T.Tbl.t; (* predicate definitions *)
+    needs_th_combination: LE.t T.Tbl.t; (* terms that require theory combination *)
+    t_defs: LE.t T.Tbl.t; (* term definitions *)
+    pred_defs: (pred * LE.t * LE.t * T.t * T.t) T.Tbl.t; (* predicate definitions *)
+    local_eqs: (N.t * N.t) Backtrack_stack.t; (* inferred by the congruence closure *)
   }
 
   let create tst : state =
@@ -116,10 +141,20 @@ module Make(A : ARG) : S with module A = A = struct
       simps=T.Tbl.create 128;
       gensym=A.Gensym.create tst;
       neq_encoded=T.Tbl.create 16;
-      t_defs=[];
+      needs_th_combination=T.Tbl.create 8;
+      t_defs=T.Tbl.create 8;
       pred_defs=T.Tbl.create 16;
+      local_eqs = Backtrack_stack.create();
     }
 
+  let push_level self =
+    Backtrack_stack.push_level self.local_eqs;
+    ()
+
+  let pop_levels self n =
+    Backtrack_stack.pop_levels self.local_eqs n ~f:(fun _ -> ());
+    ()
+
   (* FIXME
   let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
     let tst = self.tst in
@@ -191,71 +226,119 @@ module Make(A : ARG) : S with module A = A = struct
       LE.( n * t )
     | LRA_const q -> LE.of_const q
 
+  let as_linexp_id = as_linexp ~f:CCFun.id
+
   (* TODO: keep the linexps until they're asserted;
      TODO: but use simplification in preprocess
      *)
 
   (* preprocess linear expressions away *)
-  let preproc_lra self si ~recurse ~mk_lit:_ ~add_clause:_ (t:T.t) : T.t option =
+  let preproc_lra (self:state) si ~recurse ~mk_lit:_ ~add_clause:_ (t:T.t) : T.t option =
     Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t);
-    let _tst = SI.tst si in
+    let tst = SI.tst si in
     match A.view_as_lra t with
+    | LRA_pred ((Eq|Neq) as pred, t1, t2) ->
+      (* keep equality as is, needed for congruence closure *)
+      let t1 = recurse t1 in
+      let t2 = recurse t2 in
+      let u = A.mk_lra tst (LRA_pred (pred, t1, t2)) in
+      if T.equal t u then None else Some u
     | LRA_pred (pred, t1, t2) ->
       let l1 = as_linexp ~f:recurse t1 in
       let l2 = as_linexp ~f:recurse t2 in
       let proxy = fresh_term self ~pre:"_pred_lra_" Ty.bool in
-      T.Tbl.add self.pred_defs proxy (pred, l1, l2);
+      T.Tbl.add self.pred_defs proxy (pred, l1, l2, t1, t2);
       Log.debugf 5 (fun k->k"@[<hv2>lra.preprocess.step %a@ :into %a@ :def %a@]"
                        T.pp t T.pp proxy pp_pred_def (pred,l1,l2));
       Some proxy
     | LRA_op _ | LRA_mult _ ->
       let le = as_linexp ~f:recurse t in
       let proxy = fresh_term self ~pre:"_e_lra_" (T.ty t) in
-      self.t_defs <- (proxy, le) :: self.t_defs;
+      T.Tbl.add self.t_defs proxy le;
+      T.Tbl.add self.needs_th_combination proxy le;
       Log.debugf 5 (fun k->k"@[<hv2>lra.preprocess.step %a@ :into %a@ :def %a@]"
                        T.pp t T.pp proxy LE.pp le);
       Some proxy
+    | LRA_other t when A.has_ty_real t ->
+      let le = LE.monomial1 t in
+      T.Tbl.replace self.needs_th_combination t le;
+      None
     | LRA_const _ | LRA_other _ -> None
 
-  (* partial check: just ensure [a != b] triggers the clause
+  (* ensure that [a != b] triggers the clause
      [a=b \/ a<b \/ a>b] *)
-  let partial_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =
+  let encode_neq self si acts trail : unit =
     let tst = self.tst in
     begin
       trail
-      |> Iter.filter (fun lit -> not (Lit.sign lit))
       |> Iter.filter_map
         (fun lit ->
            let t = Lit.term lit in
-           match A.view_as_lra t with
-           | LRA_pred (Eq, a, b) when not (T.Tbl.mem self.neq_encoded t) ->
-             Some (lit, a,b)
-           | _ -> None)
+           Log.debugf 50 (fun k->k "@[lra: check lit %a@ :t %a@ :sign %B@]"
+                             Lit.pp lit T.pp t (Lit.sign lit));
+
+           let check_pred pred a b =
+             let pred = if Lit.sign lit then pred else Predicate.neg pred in
+             Log.debugf 50 (fun k->k "pred = `%s`" (Predicate.to_string pred));
+             if pred = Neq && not (T.Tbl.mem self.neq_encoded t) then (
+               Some (lit, a, b)
+             ) else None
+           in
+
+           begin match T.Tbl.find self.pred_defs t with
+             | (pred, _, _, ta, tb) -> check_pred pred ta tb
+             | exception Not_found ->
+               begin match A.view_as_lra t with
+                 | LRA_pred (pred, a, b) -> check_pred pred a b
+                 | _ -> None
+               end
+           end)
       |> Iter.iter
         (fun (lit,a,b) ->
+           Log.debugf 50 (fun k->k "encode neq in %a" Lit.pp lit);
            let c = [
-             Lit.abs lit;
+             Lit.neg lit;
              SI.mk_lit si acts (A.mk_lra tst (LRA_pred (Lt, a, b)));
              SI.mk_lit si acts (A.mk_lra tst (LRA_pred (Lt, b, a)));
            ] in
            SI.add_clause_permanent si acts c;
-           T.Tbl.add self.neq_encoded (Lit.term lit) ();
+           T.Tbl.add self.neq_encoded (Lit.term (Lit.abs lit)) ();
         )
     end
 
+  let dedup_lits lits : _ list =
+    let module LTbl = CCHashtbl.Make(Lit) in
+    let tbl = LTbl.create 16 in
+    List.iter (fun l -> LTbl.replace tbl l ()) lits;
+    LTbl.keys_list tbl
+
+  module Q_map = CCMap.Make(Q)
+
   let final_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =
     Log.debug 5 "(th-lra.final-check)";
+    Profile.with_ "lra.final-check" @@ fun () ->
     let simplex = SimpSolver.create self.gensym in
+    encode_neq self si acts trail;
     (* first, add definitions *)
     begin
-      List.iter
-        (fun (t,le) ->
+      T.Tbl.iter
+        (fun t le ->
            let open LE.Infix in
            let le = le - LE.monomial1 t in
            let c = LConstr.eq0 le in
-           SimpSolver.add_constr simplex c)
+           let lit = Tag.By_def in
+           SimpSolver.add_constr simplex c lit
+        )
         self.t_defs
     end;
+    (* add congruence closure equalities *)
+    Backtrack_stack.iter self.local_eqs
+      ~f:(fun (n1,n2) ->
+         let t1 = N.term n1 |> as_linexp_id in
+         let t2 = N.term n2 |> as_linexp_id in
+         let c = LConstr.eq0 LE.(t1 -  t2) in
+         let lit = Tag.CC_eq (n1,n2) in
+         SimpSolver.add_constr simplex c lit);
     (* add trail *)
     begin
       trail
@@ -263,37 +346,96 @@ module Make(A : ARG) : S with module A = A = struct
         (fun lit ->
            let sign = Lit.sign lit in
            let t = Lit.term lit in
+           let assert_pred pred a b =
+             let pred = if sign then pred else Predicate.neg pred in
+             if pred = Neq then (
+               Log.debugf 50 (fun k->k "(@[LRA.skip-neq@ :in %a@])" T.pp t);
+             ) else (
+               let c = LConstr.of_expr LE.(a-b) pred in
+               SimpSolver.add_constr simplex c (Tag.Lit lit);
+             )
+           in
            begin match T.Tbl.find self.pred_defs t with
-             | exception Not_found -> ()
-             | (pred, a, b) ->
-               (* FIXME: generic negation+printer in Linear_expr_intf;
-                  actually move predicates to their own module *)
-               let pred = if sign then pred else Predicate.neg pred in
-               if pred = Neq then (
-                 Log.debugf 50 (fun k->k "skip neq in %a" T.pp t);
-               ) else (
-                 (* TODO: tag *)
-                 let c = LConstr.of_expr LE.(a-b) pred in
-                 SimpSolver.add_constr simplex c;
-               )
+             | (pred, a, b, _, _) -> assert_pred pred a b
+             | exception Not_found ->
+               begin match A.view_as_lra t with
+                 | LRA_pred (pred, a, b) ->
+                   let a = try T.Tbl.find self.t_defs a with _ -> as_linexp_id a in
+                   let b = try T.Tbl.find self.t_defs b with _ -> as_linexp_id b in
+                   assert_pred pred a b
+                 | _ -> ()
+               end
            end)
     end;
     Log.debug 5 "lra: call arith solver";
-    begin match SimpSolver.solve simplex with
+    let res = Profile.with1 "simplex.solve" SimpSolver.solve simplex in
+    begin match res with
       | SimpSolver.Solution _m ->
         Log.debug 5 "lra: solver returns SAT";
-        () (* TODO: get a model + model combination *)
-      | SimpSolver.Unsatisfiable _cert ->
-        (* we tagged assertions with their lit, so the certificate being an
-           unsat core translates directly into a conflict clause *)
-        assert false
-          (* TODO
+        Log.debugf 50
+          (fun k->k "(@[LRA.needs-th-combination:@ %a@])"
+              (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination));
+        (* FIXME: theory combination
+        let lazy model = model in
+        Log.debugf 30 (fun k->k "(@[LRA.model@ %a@])" FM_A.pp_model model);
+
+        (* theory combination: for [t1,t2] terms in [self.needs_th_combination]
+           that have same value, but are not provably equal, push
+           decision [t1=t2] into the SAT solver. *)
+        begin
+          let by_val: T.t list Q_map.t =
+            T.Tbl.to_iter self.needs_th_combination
+            |> Iter.map (fun (t,le) -> FM_A.eval_model model le, t)
+            |> Iter.fold
+              (fun m (q,t) ->
+                 let l = Q_map.get_or ~default:[] q m in
+                 Q_map.add q (t::l) m)
+              Q_map.empty
+          in
+          Q_map.iter
+            (fun _q ts ->
+               begin match ts with
+                 | [] | [_] -> ()
+                 | ts ->
+                   (* several terms! see if they are already equal *)
+                   CCList.diagonal ts
+                   |> List.iter
+                     (fun (t1,t2) ->
+                        Log.debugf 50
+                          (fun k->k "(@[LRA.th-comb.check-pair[val=%a]@ %a@ %a@])"
+                              Q.pp_print _q T.pp t1 T.pp t2);
+                        (* FIXME: we need these equalities to be considered
+                           by the congruence closure *)
+                        if not (SI.cc_are_equal si t1 t2) then (
+                          Log.debug 50 "LRA.th-comb.must-decide-equal";
+                          let t = A.mk_lra (SI.tst si) (LRA_pred (Eq, t1, t2)) in
+                          let lit = SI.mk_lit si acts t in
+                          SI.push_decision si acts lit
+                        )
+                     )
+               end)
+            by_val;
+          ()
+        end;
+           *)
+        ()
+      | SimpSolver.Unsatisfiable cert ->
+        let unsat_core =
+          match SimpSolver.check_cert simplex cert with
+          | `Ok unsat_core -> unsat_core (* TODO *)
+          | _ -> assert false (* some kind of fatal error ? *)
+        in
         Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a"
-                         (Fmt.Dump.list Lit.pp) lits);
-        let confl = List.rev_map Lit.neg lits in
+                         (Fmt.Dump.list Tag.pp) unsat_core);
         (* TODO: produce and store a proper LRA resolution proof *)
+        let confl =
+          unsat_core
+          |> Iter.of_list
+          |> Iter.flat_map_l (fun tag -> Tag.to_lits si tag)
+          |> Iter.map Lit.neg
+          |> Iter.to_rev_list
+        in
         SI.raise_conflict si acts confl SI.P.default
-             *)
     end;
     ()
 
@@ -302,8 +444,12 @@ module Make(A : ARG) : S with module A = A = struct
     let st = create (SI.tst si) in
     (* TODO    SI.add_simplifier si (simplify st); *)
     SI.add_preprocess si (preproc_lra st);
-    SI.on_partial_check si (partial_check_ st);
     SI.on_final_check si (final_check_ st);
+    SI.on_cc_post_merge si
+      (fun _ _ n1 n2 ->
+         if A.has_ty_real (N.term n1) then (
+           Backtrack_stack.push st.local_eqs (n1, n2)
+         ));
     (*     SI.add_preprocess si (cnf st); *)
     (* TODO: theory combination *)
     st
@@ -311,6 +457,6 @@ module Make(A : ARG) : S with module A = A = struct
   let theory =
     A.S.mk_theory
       ~name:"th-lra"
-      ~create_and_setup
+      ~create_and_setup ~push_level ~pop_levels
       ()
 end
diff --git a/src/arith/lra/simplex.ml b/src/arith/lra/simplex.ml
index b0946208..e12224ac 100644
--- a/src/arith/lra/simplex.ml
+++ b/src/arith/lra/simplex.ml
@@ -122,13 +122,18 @@ module Make_inner
   let str_of_erat = Format.to_string Erat.pp
   let str_of_q = Format.to_string Q.pp_print
 
+  type bound = {
+    value : Erat.t;
+    reason : lit option;
+  }
+
   type t = {
     param: param;
     tab : Q.t Matrix.t; (* the matrix of coefficients *)
     basic : basic_var Vec.vector; (* basic variables *)
     nbasic : nbasic_var Vec.vector; (* non basic variables *)
     mutable assign : Erat.t M.t; (* assignments *)
-    mutable bounds : (Erat.t * Erat.t) M.t; (* (lower, upper) bounds for variables *)
+    mutable bounds : (bound * bound) M.t; (* (lower, upper) bounds for variables *)
     mutable idx_basic : int M.t; (* basic var -> its index in [basic] *)
     mutable idx_nbasic : int M.t; (* non basic var -> its index in [nbasic] *)
   }
@@ -136,7 +141,6 @@ module Make_inner
   type cert = {
     cert_var: var;
     cert_expr: (Q.t * var) list;
-    cert_core: lit list;
   }
 
   type res =
@@ -239,17 +243,23 @@ module Make_inner
     with Not_found -> value_basic t x
 
   (* trivial bounds *)
-  let empty_bounds : Erat.t * Erat.t = Q.(Erat.make minus_inf zero, Erat.make inf zero)
+  let empty_bounds : bound * bound =
+    { value = Erat.make Q.minus_inf Q.zero; reason = None; },
+    { value = Erat.make Q.inf Q.zero; reason = None; }
 
   (* find bounds of [x] *)
-  let[@inline] get_bounds (t:t) (x:var) : Erat.t * Erat.t =
+  let[@inline] get_bounds (t:t) (x:var) : bound * bound =
     try M.find x t.bounds
     with Not_found -> empty_bounds
 
+  let[@inline] get_bounds_values (t:t) (x:var) : Erat.t * Erat.t =
+    let l, u = get_bounds t x in
+    l.value, u.value
+
   (* is [value x] within the bounds for [x]? *)
   let is_within_bounds (t:t) (x:var) : bool * Erat.t =
     let v = value t x in
-    let low, upp = get_bounds t x in
+    let low, upp = get_bounds_values t x in
     if Erat.compare v low < 0 then
       false, low
     else if Erat.compare v upp > 0 then
@@ -313,15 +323,21 @@ module Make_inner
     ()
 
   (* add bounds to [x] in [t] *)
-  let add_bound_aux (t:t) (x:var) (low:Erat.t) (upp:Erat.t) : unit =
+  let add_bound_aux (t:t) (x:var)
+      (low:Erat.t) (low_reason:lit option)
+      (upp:Erat.t) (upp_reason:lit option) : unit =
     add_vars t [x];
     let l, u = get_bounds t x in
-    t.bounds <- M.add x (Erat.max l low, Erat.min u upp) t.bounds
+    let l' = if Erat.lt low l.value then l else { value = low; reason = low_reason; } in
+    let u' = if Erat.gt upp u.value then u else { value = upp; reason = upp_reason; } in
+    t.bounds <- M.add x (l', u') t.bounds
 
-  let add_bounds (t:t) ?strict_lower:(slow=false) ?strict_upper:(supp=false) (x, l, u) : unit =
+  let add_bounds (t:t)
+      ?strict_lower:(slow=false) ?strict_upper:(supp=false)
+      ?lower_reason ?upper_reason (x, l, u) : unit =
     let e1 = if slow then Q.one else Q.zero in
     let e2 = if supp then Q.neg Q.one else Q.zero in
-    add_bound_aux t x (Erat.make l e1) (Erat.make u e2);
+    add_bound_aux t x (Erat.make l e1) lower_reason (Erat.make u e2) upper_reason;
     if mem_nbasic t x then (
       let b, v = is_within_bounds t x in
       if not b then (
@@ -329,8 +345,11 @@ module Make_inner
       )
     )
 
-  let add_lower_bound t ?strict x l = add_bounds t ?strict_lower:strict (x,l,Q.inf)
-  let add_upper_bound t ?strict x u = add_bounds t ?strict_upper:strict (x,Q.minus_inf,u)
+  let add_lower_bound t ?strict ~reason x l =
+    add_bounds t ?strict_lower:strict ~lower_reason:reason (x,l,Q.inf)
+
+  let add_upper_bound t ?strict ~reason x u =
+    add_bounds t ?strict_upper:strict ~upper_reason:reason (x,Q.minus_inf,u)
 
   (* full assignment *)
   let full_assign (t:t) : (var * Erat.t) Iter.t =
@@ -352,7 +371,8 @@ module Make_inner
   let solve_epsilon (t:t) : Q.t =
     let emax =
       M.fold
-        (fun x ({base=low;eps_factor=e_low}, {base=upp;eps_factor=e_upp}) emax ->
+        (fun x ({ value = {base=low;eps_factor=e_low}; _},
+                { value = {base=upp;eps_factor=e_upp}; _}) emax ->
            let {base=v; eps_factor=e_v} = value t x in
            (* lower bound *)
            let emax =
@@ -396,7 +416,7 @@ module Make_inner
     let test (y:nbasic_var) (a:Q.t) : bool =
       assert (mem_nbasic t y);
       let v = value t y in
-      let low, upp = get_bounds t y in
+      let low, upp = get_bounds_values t y in
       if b then (
         (Erat.lt v upp && Q.compare a Q.zero > 0) ||
         (Erat.gt v low && Q.compare a Q.zero < 0)
@@ -489,7 +509,7 @@ module Make_inner
 
   (* check bounds *)
   let check_bounds (t:t) : unit =
-    M.iter (fun x (l, u) -> if Erat.gt l u then raise (AbsurdBounds x)) t.bounds
+    M.iter (fun x (l, u) -> if Erat.gt l.value u.value then raise (AbsurdBounds x)) t.bounds
 
   (* actual solving algorithm *)
   let solve_aux (t:t) : unit =
@@ -534,9 +554,9 @@ module Make_inner
             (Vec.to_list (find_expr_basic t x))
             (Vec.to_list t.nbasic)
         in
-        Unsatisfiable { cert_var=x; cert_expr; cert_core=[]; } (* FIXME *)
+        Unsatisfiable { cert_var=x; cert_expr; } (* FIXME *)
       | AbsurdBounds x ->
-        Unsatisfiable { cert_var=x; cert_expr=[]; cert_core=[]; }
+        Unsatisfiable { cert_var=x; cert_expr=[]; }
 
   (* add [c·x] to [m] *)
   let add_expr_ (x:var) (c:Q.t) (m:Q.t M.t) =
@@ -557,38 +577,54 @@ module Make_inner
       !m
 
   (* maybe invert bounds, if [c < 0] *)
-  let scale_bounds c (l,u) : erat * erat =
+  let scale_bounds c (l,u) : bound * bound =
     match Q.compare c Q.zero with
-      | 0 -> Erat.zero, Erat.zero
-      | n when n<0 -> Erat.mul c u, Erat.mul c l
-      | _ -> Erat.mul c l, Erat.mul c u
+      | 0 ->
+        let b = { value = Erat.zero; reason = None; } in
+        b, b
+      | n when n<0 ->
+        { u with value = Erat.mul c u.value; },
+        { l with value = Erat.mul c l.value; }
+      | _ ->
+        { l with value = Erat.mul c l.value; },
+        { u with value = Erat.mul c u.value; }
+
+  let add_to_unsat_core acc = function
+    | None -> acc
+    | Some reason -> reason :: acc
 
   let check_cert (t:t) (c:cert) =
     let x = c.cert_var in
-    let low_x, up_x = get_bounds t x in
+    let { value = low_x; reason = low_x_reason; },
+        { value = up_x; reason = upp_x_reason; } = get_bounds t x in
     begin match c.cert_expr with
       | [] ->
-        if Erat.compare low_x up_x > 0 then `Ok
+        if Erat.compare low_x up_x > 0
+        then `Ok (add_to_unsat_core (add_to_unsat_core [] low_x_reason) upp_x_reason)
         else `Bad_bounds (str_of_erat low_x, str_of_erat up_x)
       | expr ->
         let e0 = deref_var_ t x (Q.neg Q.one) M.empty in
         (* compute bounds for the expression [c.cert_expr],
            and also compute [c.cert_expr - x] to check if it's 0] *)
-        let low, up, expr_minus_x =
+        let low, low_unsat_core, up, up_unsat_core, expr_minus_x =
           List.fold_left
-            (fun (l,u,expr_minus_x) (c, y) ->
+            (fun (l, luc, u, uuc, expr_minus_x) (c, y) ->
                let ly, uy = scale_bounds c (get_bounds t y) in
-               assert (Erat.compare ly uy <= 0);
+               assert (Erat.compare ly.value uy.value <= 0);
                let expr_minus_x = deref_var_ t y c expr_minus_x in
-               Erat.sum l ly, Erat.sum u uy, expr_minus_x)
-              (Erat.zero, Erat.zero, e0)
+               let luc = add_to_unsat_core luc ly.reason in
+               let uuc = add_to_unsat_core uuc uy.reason in
+               Erat.sum l ly.value, luc, Erat.sum u uy.value, uuc, expr_minus_x)
+            (Erat.zero, [], Erat.zero, [], e0)
               expr
         in
         (* check that the expanded expression is [x], and that
            one of the bounds on [x] is incompatible with bounds of [c.cert_expr] *)
         if M.is_empty expr_minus_x then (
-          if Erat.compare low_x up > 0 || Erat.compare up_x low < 0
-          then `Ok
+          if Erat.compare low_x up > 0
+          then `Ok (add_to_unsat_core up_unsat_core low_x_reason)
+          else if Erat.compare up_x low < 0
+          then `Ok (add_to_unsat_core low_unsat_core upp_x_reason)
           else `Bad_bounds (str_of_erat low, str_of_erat up)
         ) else `Diff_not_0 expr_minus_x
     end
@@ -631,14 +667,14 @@ module Make_inner
     let pp_pair =
       within "(" ")" @@ hvbox @@ pair ~sep:(return "@ := ") Var.pp Erat.pp
     in
-    map Var_map.to_seq @@ within "(" ")" @@ hvbox @@ seq pp_pair
+    map Var_map.to_iter @@ within "(" ")" @@ hvbox @@ iter pp_pair
 
   let pp_bounds =
     let open Format in
     let pp_pairs out (x,(l,u)) =
-      fprintf out "(@[%a =< %a =< %a@])" Erat.pp l Var.pp x Erat.pp u
+      fprintf out "(@[%a =< %a =< %a@])" Erat.pp l.value Var.pp x Erat.pp u.value
     in
-    map Var_map.to_seq @@ within "(" ")" @@ hvbox @@ seq pp_pairs
+    map Var_map.to_iter @@ within "(" ")" @@ hvbox @@ iter pp_pairs
 
   let pp_full_state out (t:t) : unit =
     (* print main matrix *)
@@ -659,6 +695,13 @@ module Make_full_for_expr(V : VAR_GEN)
      with type Var.t = V.t
       and type C.t = Q.t
       and type Var.lit = V.lit)
+  : S_FULL with type var = V.t
+            and type lit = V.lit
+            and module L = L
+            and module Var_map = L.Var_map
+            and type L.var = V.t
+            and type L.Comb.t = L.Comb.t
+            and type param = V.Fresh.t
 = struct
   include Make_inner(V)(L.Var_map)(V.Fresh)
   module L = L
@@ -668,19 +711,25 @@ module Make_full_for_expr(V : VAR_GEN)
   type constr = L.Constr.t
 
   (* add a constraint *)
-  let add_constr (t:t) (c:constr) : unit =
+  let add_constr (t:t) (c:constr) (reason:lit) : unit =
     let (x:var) = V.Fresh.fresh t.param in
     let e, op, q = L.Constr.split c in
     add_eq t (x, L.Comb.to_list e);
     begin match op with
-      | Leq -> add_upper_bound t ~strict:false x q
-      | Geq -> add_lower_bound t ~strict:false x q
-      | Lt -> add_upper_bound t ~strict:true x q
-      | Gt -> add_lower_bound t ~strict:true x q
-      | Eq -> add_bounds t ~strict_lower:false ~strict_upper:false (x,q,q)
+      | Leq -> add_upper_bound t ~strict:false ~reason x q
+      | Geq -> add_lower_bound t ~strict:false ~reason x q
+      | Lt -> add_upper_bound t ~strict:true ~reason x q
+      | Gt -> add_lower_bound t ~strict:true ~reason x q
+      | Eq -> add_bounds t (x,q,q)
+                ~strict_lower:false ~strict_upper:false
+                ~lower_reason:reason ~upper_reason:reason
       | Neq -> assert false
     end
 end
 
 module Make_full(V : VAR_GEN)
+  : S_FULL with type var = V.t
+            and type lit = V.lit
+            and type L.var = V.t
+            and type param = V.Fresh.t
   = Make_full_for_expr(V)(Linear_expr.Make(struct include Q let pp = pp_print end)(V))
diff --git a/src/arith/lra/simplex.mli b/src/arith/lra/simplex.mli
index 9fc81194..8bbcef5d 100644
--- a/src/arith/lra/simplex.mli
+++ b/src/arith/lra/simplex.mli
@@ -22,6 +22,8 @@ module Make_full_for_expr(V : VAR_GEN)
             and type lit = V.lit
             and module L = L
             and module Var_map = L.Var_map
+            and type L.var = V.t
+            and type L.Comb.t = L.Comb.t
             and type param = V.Fresh.t
 
 module Make_full(V : VAR_GEN)
diff --git a/src/arith/lra/simplex_intf.ml b/src/arith/lra/simplex_intf.ml
index e1ed0e90..2e5d18f6 100644
--- a/src/arith/lra/simplex_intf.ml
+++ b/src/arith/lra/simplex_intf.ml
@@ -35,7 +35,6 @@ module type S = sig
   type cert = {
     cert_var: var;
     cert_expr: (Q.t * var) list;
-    cert_core: lit list;
   }
 
   (** Generic type returned when solving the simplex. A solution is a list of
@@ -66,11 +65,14 @@ module type S = sig
       [Q.inf].
       Optional parameters allow to make the the bounds strict. Defaults to false,
       so that bounds are large by default. *)
-  val add_bounds : t -> ?strict_lower:bool -> ?strict_upper:bool -> var * Q.t * Q.t -> unit
+  val add_bounds : t ->
+    ?strict_lower:bool -> ?strict_upper:bool ->
+    ?lower_reason:lit -> ?upper_reason:lit ->
+    var * Q.t * Q.t -> unit
 
-  val add_lower_bound : t -> ?strict:bool -> var -> Q.t -> unit
+  val add_lower_bound : t -> ?strict:bool -> reason:lit -> var -> Q.t -> unit
 
-  val add_upper_bound : t -> ?strict:bool -> var -> Q.t -> unit
+  val add_upper_bound : t -> ?strict:bool -> reason:lit -> var -> Q.t -> unit
 
   (** {3 Simplex solving} *)
 
@@ -85,10 +87,10 @@ module type S = sig
   val check_cert :
     t ->
     cert ->
-    [`Ok | `Bad_bounds of string * string | `Diff_not_0 of Q.t Var_map.t]
+    [`Ok of lit list | `Bad_bounds of string * string | `Diff_not_0 of Q.t Var_map.t]
   (** checks that the certificat indeed yields to a contradiction
       in the current state of the simplex.
-      @return [`Ok] if the certificate is valid. *)
+      @return [`Ok unsat_core] if the certificate is valid. *)
 
   (* TODO: push/pop? at least on bounds *)
 
@@ -119,6 +121,6 @@ module type S_FULL = sig
 
   type constr = L.Constr.t
 
-  val add_constr : t -> constr -> unit
+  val add_constr : t -> constr -> lit -> unit
   (** Add a constraint to a simplex state. *)
 end
diff --git a/src/arith/tests/run_tests.ml b/src/arith/tests/run_tests.ml
index 6cea0b45..a1345c65 100644
--- a/src/arith/tests/run_tests.ml
+++ b/src/arith/tests/run_tests.ml
@@ -1,6 +1,4 @@
 
-open OUnit
-
 let props =
   List.flatten
     [ Test_simplex.props;
diff --git a/src/arith/tests/test_simplex.ml b/src/arith/tests/test_simplex.ml
index 97a4f084..ac0c7fbd 100644
--- a/src/arith/tests/test_simplex.ml
+++ b/src/arith/tests/test_simplex.ml
@@ -107,11 +107,13 @@ module Problem = struct
     QC.list_of_size QC.Gen.(m -- n) @@ Constr.rand 10
 end
 
-let add_problem (t:Spl.t) (pb:Problem.t) : unit = List.iter (Spl.add_constr t) pb
+let add_problem (t:Spl.t) (pb:Problem.t) : unit =
+  let lit = 0 in
+  List.iter (fun constr -> Spl.add_constr t constr lit) pb
 
 let pp_subst : subst Fmt.printer =
-  Fmt.(map Spl.L.Var_map.to_seq @@
-    within "{" "}" @@ hvbox @@ seq ~sep:(return ",@ ") @@
+  Fmt.(map Spl.L.Var_map.to_iter @@
+    within "{" "}" @@ hvbox @@ iter ~sep:(return ",@ ") @@
     pair ~sep:(return "@ @<1>→ ") Var.pp Q.pp_print
   )
 
@@ -150,7 +152,7 @@ let check_sound =
         )
       | Spl.Unsatisfiable cert ->
         begin match Spl.check_cert simplex cert with
-          | `Ok -> true
+          | `Ok _ -> true
           | `Bad_bounds (low, up) ->
             QC.Test.fail_reportf
               "(@[<hv>bad-certificat@ :problem %a@ :cert %a@ :low %s :up %s@ :simplex-after  %a@ :simplex-before %a@])"
diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 74de8767..47c421a5 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -373,6 +373,7 @@ module Make (A: CC_ARG)
     end
 
   let raise_conflict (cc:t) ~th (acts:actions) (e:lit list) : _ =
+    Profile.instant "cc.conflict";
     (* clear tasks queue *)
     Vec.clear cc.pending;
     Vec.clear cc.combine;
@@ -835,6 +836,10 @@ module Make (A: CC_ARG)
   let[@inline] merge_t cc t1 t2 expl =
     merge cc (add_term cc t1) (add_term cc t2) expl
 
+  let explain_eq cc n1 n2 : lit list =
+    let th = ref true in
+    explain_pair cc ~th [] n1 n2
+
   let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge
   let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_merge
   let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 127aa65d..7ef211bd 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -280,6 +280,10 @@ module type CC_S = sig
   val assert_lits : t -> lit Iter.t -> unit
   (** Addition of many literals *)
 
+  val explain_eq : t -> N.t -> N.t -> lit list
+  (** Explain why the two nodes are equal.
+      Fails if they are not, in an unspecified way *)
+
   val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
   (** Raise a conflict with the given explanation
       it must be a theory tautology that [expl ==> absurd].
@@ -390,10 +394,19 @@ module type SOLVER_INTERNAL = sig
   (** {3 hooks for the theory} *)
 
   val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit
+  (** Propagate a literal for a reason. This is similar to asserting
+      the clause [reason => lit], but more lightweight, and in a way
+      that is backtrackable. *)
 
   val raise_conflict : t -> actions -> lit list -> proof -> 'a
   (** Give a conflict clause to the solver *)
 
+  val push_decision : t -> actions -> lit -> unit
+  (** Ask the SAT solver to decide the given literal in an extension of the
+      current trail. This is useful for theory combination.
+      If the SAT solver backtracks, this (potential) decision is removed
+      and forgotten. *)
+
   val propagate: t -> actions -> lit -> (unit -> lit list) -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
@@ -429,6 +442,9 @@ module type SOLVER_INTERNAL = sig
   val cc_find : t -> CC.N.t -> CC.N.t
   (** Find representative of the node *)
 
+  val cc_are_equal : t -> term -> term -> bool
+  (** Are these two terms equal in the congruence closure? *)
+
   val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
   (** Merge these two nodes in the congruence closure, given this explanation.
       It must be a theory tautology that [expl ==> n1 = n2].
diff --git a/src/main/dune b/src/main/dune
index 77c68d7a..5a8ae94c 100644
--- a/src/main/dune
+++ b/src/main/dune
@@ -5,7 +5,7 @@
  (public_name sidekick)
  (package sidekick-bin)
  (libraries containers iter result msat sidekick.core sidekick-arith.base-term
-   sidekick.msat-solver sidekick-bin.smtlib)
+   sidekick.msat-solver sidekick-bin.smtlib sidekick.tef)
  (flags :standard -safe-string -color always -open Sidekick_util))
 
 (rule
diff --git a/src/main/main.ml b/src/main/main.ml
index 001d8330..5c1cf236 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -78,6 +78,7 @@ let argspec = Arg.align [
     "--no-p", Arg.Clear p_progress, " no progress bar";
     "--size", Arg.String (int_arg size_limit), " <s>[kMGT] sets the size limit for the sat solver";
     "--time", Arg.String (int_arg time_limit), " <t>[smhd] sets the time limit for the sat solver";
+    "-t", Arg.String (int_arg time_limit), " short for --time";
     "--version", Arg.Unit (fun () -> Printf.printf "version: %s\n%!" Sidekick_version.version; exit 0), " show version and exit";
     "-d", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
     "--debug", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
@@ -126,6 +127,8 @@ let check_limits () =
     raise Out_of_space
 
 let main () =
+  Sidekick_tef.setup();
+  at_exit Sidekick_tef.teardown;
   CCFormat.set_color_default true;
   (* Administrative duties *)
   Arg.parse argspec input_file usage;
diff --git a/src/mini-cc/Sidekick_mini_cc.ml b/src/mini-cc/Sidekick_mini_cc.ml
index 557beda7..33f64853 100644
--- a/src/mini-cc/Sidekick_mini_cc.ml
+++ b/src/mini-cc/Sidekick_mini_cc.ml
@@ -147,13 +147,14 @@ module Make(A: ARG) = struct
     self
 
   let clear (self:t) : unit =
+    let {ok=_; tbl; sig_tbl; pending=_; combine=_; true_; false_} = self in
     self.ok <- true;
-    T_tbl.clear self.tbl;
-    Sig_tbl.clear self.sig_tbl;
     self.pending <- [];
     self.combine <- [];
-    T_tbl.add self.tbl self.true_.n_t self.true_;
-    T_tbl.add self.tbl self.false_.n_t self.false_;
+    T_tbl.clear tbl;
+    Sig_tbl.clear sig_tbl;
+    T_tbl.add tbl true_.n_t true_;
+    T_tbl.add tbl false_.n_t false_;
     ()
 
   let sub_ t k : unit =
@@ -317,5 +318,4 @@ module Make(A: ARG) = struct
     |> Iter.filter Node.is_root
     |> Iter.map
       (fun n -> Node.iter_cls n |> Iter.map Node.term)
-    
 end
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index b5036682..5dc47f53 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -202,6 +202,10 @@ module Make(A : ARG)
 
     let add_preprocess self f = self.preprocess <- f :: self.preprocess
 
+    let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
+      let sign = Lit.sign lit in
+      acts.Msat.acts_add_decision_lit (Lit.abs lit) sign
+
     let[@inline] raise_conflict self acts c : 'a =
       Stat.incr self.count_conflict;
       acts.Msat.acts_raise_conflict c P.default
@@ -279,6 +283,10 @@ module Make(A : ARG)
 
     let cc_add_term self t = CC.add_term (cc self) t
     let cc_find self n = CC.find (cc self) n
+    let cc_are_equal self t1 t2 =
+      let n1 = cc_add_term self t1 in
+      let n2 = cc_add_term self t2 in
+      N.equal (cc_find self n1) (cc_find self n2)
     let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e
     let cc_merge_t self acts t1 t2 e =
       cc_merge self acts (cc_add_term self t1) (cc_add_term self t2) e
@@ -345,10 +353,12 @@ module Make(A : ARG)
 
     (* propagation from the bool solver *)
     let check_ ~final (self:t) (acts: msat_acts) =
+      let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in
       let iter = iter_atoms_ acts in
       Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
       self.on_progress();
-      assert_lits_ ~final self acts iter
+      assert_lits_ ~final self acts iter;
+      Profile.exit pb
 
     (* propagation from the bool solver *)
     let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
@@ -578,13 +588,16 @@ module Make(A : ARG)
 
   let add_clause (self:t) (c:Atom.t IArray.t) : unit =
     Stat.incr self.count_clause;
-    Log.debugf 50 (fun k->k "add clause %a@." (Util.pp_iarray Atom.pp) c);
-    Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default
+    Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Atom.pp) c);
+    let pb = Profile.begin_ "add-clause" in
+    Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default;
+    Profile.exit pb
 
   let add_clause_l self c = add_clause self (IArray.of_list c)
 
   let mk_model (self:t) (lits:lit Iter.t) : Model.t =
     Log.debug 1 "(smt.solver.mk-model)";
+    Profile.with_ "msat-solver.mk-model" @@ fun () ->
     let module M = Term.Tbl in
     let m = M.create 128 in
     let tst = self.si.tst in
@@ -606,6 +619,7 @@ module Make(A : ARG)
 
   let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ())
       ~assumptions (self:t) : res =
+    Profile.with_ "msat-solver.solve" @@ fun () ->
     let do_on_exit () =
       List.iter (fun f->f()) on_exit;
     in
diff --git a/src/smtlib/Form.ml b/src/smtlib/Form.ml
index 417fd943..2dc21cfc 100644
--- a/src/smtlib/Form.ml
+++ b/src/smtlib/Form.ml
@@ -134,6 +134,7 @@ let imply_l st xs y = match xs with
   | _ -> T.app_fun st Funs.imply (IArray.of_list @@ y :: xs)
 
 let imply st a b = imply_a st (IArray.singleton a) b
+let xor st a b = not_ st (equiv st a b)
 
 let distinct_l tst l =
   match l with
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 06d1aa23..a6e72523 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -1,6 +1,7 @@
 (** {2 Conversion into {!Term.t}} *)
 
 module BT = Sidekick_base_term
+module Profile = Sidekick_util.Profile
 open Sidekick_base_term
 
 [@@@ocaml.warning "-32"]
@@ -153,8 +154,10 @@ let solve
   let on_progress =
     if progress then Some (mk_progress()) else None in
   let res =
-    Solver.solve ~assumptions ?on_progress s
+    Profile.with_ "solve" begin fun () ->
+      Solver.solve ~assumptions ?on_progress s
     (* ?gc ?restarts ?time ?memory ?progress *)
+    end
   in
   let t2 = Sys.time () in
   Printf.printf "\r"; flush stdout;
@@ -176,11 +179,12 @@ let solve
       Format.printf "Unsat (%.3f/%.3f/-)@." t1 (t2-.t1);
     | Solver.Unsat {proof=Some p;_} ->
       if check then (
-        Solver.Proof.check p;
+        Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p);
       );
       begin match dot_proof with
         | None ->  ()
         | Some file ->
+          Profile.with_ "dot.proof" @@ fun () ->
           CCIO.with_out file
             (fun oc ->
                Log.debugf 1 (fun k->k "write proof into `%s`" file);
@@ -315,6 +319,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
     | _ -> LRA_other t
 
   let ty_lra _st = Ty.real
+  let has_ty_real t = Ty.equal (T.ty t) Ty.real
 
   module Gensym = struct
     type t = {
diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml
index ce89c1d4..17df956b 100644
--- a/src/smtlib/Typecheck.ml
+++ b/src/smtlib/Typecheck.ml
@@ -144,6 +144,10 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
             errorf_ctx ctx "expected term, not type; got `%s`" f
         end
     end
+  | PA.App ("xor", [a;b]) ->
+    let a = conv_term ctx a in
+    let b = conv_term ctx b in
+    Form.xor ctx.tst a b
   | PA.App (f, args) ->
     let args = List.map (conv_term ctx) args in
     begin match find_id_ ctx f with
@@ -280,6 +284,12 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
       | PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b))
       | PA.Add, (a::l) ->
         List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Plus,a,b))) a l
+      | PA.Minus, [a] ->
+        begin match t_as_q a with
+          | Some a -> T.lra ctx.tst (LRA_const (Q.neg a))
+          | None ->
+            T.lra ctx.tst (LRA_op (Minus, T.lra ctx.tst (LRA_const Q.zero), a))
+        end
       | PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b))
       | PA.Minus, (a::l) ->
         List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Minus,a,b))) a l
diff --git a/src/smtlib/dune b/src/smtlib/dune
index e3230bbf..2e0a0136 100644
--- a/src/smtlib/dune
+++ b/src/smtlib/dune
@@ -3,5 +3,6 @@
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith msat sidekick.core sidekick.util
    sidekick.msat-solver sidekick-arith.base-term sidekick.th-bool-static
-   sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils)
+   sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils
+   sidekick.tef)
  (flags :standard -warn-error -a+8 -open Sidekick_util))
diff --git a/src/tef/Sidekick_tef.ml b/src/tef/Sidekick_tef.ml
new file mode 100644
index 00000000..5b7467b1
--- /dev/null
+++ b/src/tef/Sidekick_tef.ml
@@ -0,0 +1,74 @@
+
+module P = Sidekick_util.Profile
+
+let active = lazy (
+  match Sys.getenv "TEF" with
+  | "1"|"true" -> true | _ -> false
+  | exception Not_found -> false
+)
+
+let program_start = Mtime_clock.now()
+
+module Make()
+  : P.BACKEND
+= struct
+  let first_ = ref true
+  let closed_ = ref false
+
+  let teardown_ oc =
+    if not !closed_ then (
+      closed_ := true;
+      output_char oc ']'; (* close array *)
+      flush oc;
+      close_out_noerr oc
+    )
+
+  (* connection to subprocess writing into the file *)
+  let oc =
+    let oc = Unix.open_process_out "gzip - --stdout > trace.json.gz" in
+    output_char oc '[';
+    at_exit (fun () -> teardown_ oc);
+    oc
+
+  let get_ts () : float =
+    let now = Mtime_clock.now() in
+    Mtime.Span.to_us (Mtime.span program_start now)
+
+  let emit_sep_ () =
+    if !first_ then (
+      first_ := false;
+    ) else (
+      output_string oc ",\n";
+    )
+
+  let emit_duration_event ~name ~start ~end_ () : unit =
+    let dur = end_ -. start in
+    let ts = start in
+    let pid = Unix.getpid() in
+    let tid = Thread.id (Thread.self()) in
+    emit_sep_();
+    Printf.fprintf oc
+      {json|{"pid": %d,"cat":"","tid": %d,"dur": %.2f,"ts": %.2f,"name":"%s","ph":"X"}|json}
+      pid tid dur ts name;
+    ()
+
+  let emit_instant_event ~name ~ts () : unit =
+    let pid = Unix.getpid() in
+    let tid = Thread.id (Thread.self()) in
+    emit_sep_();
+    Printf.fprintf oc
+      {json|{"pid": %d,"cat":"","tid": %d,"ts": %.2f,"name":"%s","ph":"I"}|json}
+      pid tid ts name;
+    ()
+
+  let teardown () = teardown_ oc
+end
+
+let setup_ = lazy (
+  let lazy active = active in
+  let b = if active then Some (module Make() : P.BACKEND) else None in
+  P.Control.setup b
+)
+
+let setup () = Lazy.force setup_
+let teardown = P.Control.teardown
diff --git a/src/tef/Sidekick_tef.mli b/src/tef/Sidekick_tef.mli
new file mode 100644
index 00000000..33168a57
--- /dev/null
+++ b/src/tef/Sidekick_tef.mli
@@ -0,0 +1,10 @@
+
+(** {1 Tracing Event Format}
+
+    A nice profiling format based on json, useful for visualizing what goes on.
+    See https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/
+*)
+
+val setup : unit -> unit
+
+val teardown : unit -> unit
diff --git a/src/tef/dune b/src/tef/dune
new file mode 100644
index 00000000..db8f8b5e
--- /dev/null
+++ b/src/tef/dune
@@ -0,0 +1,8 @@
+
+(library
+  (name sidekick_tef)
+  (public_name sidekick.tef)
+  (synopsis "profiling backend based on TEF")
+  (optional)
+  (flags :standard -warn-error -a+8)
+  (libraries sidekick.util unix threads mtime mtime.clock.os))
diff --git a/src/util/Backtrack_stack.ml b/src/util/Backtrack_stack.ml
index a23056f1..890be02f 100644
--- a/src/util/Backtrack_stack.ml
+++ b/src/util/Backtrack_stack.ml
@@ -34,3 +34,5 @@ let pop_levels (self:_ t) (n:int) ~f : unit =
     done;
     Vec.shrink self.lvls new_lvl
   )
+
+let iter ~f self = Vec.iter f self.vec
diff --git a/src/util/Backtrack_stack.mli b/src/util/Backtrack_stack.mli
index e7125138..901c63ce 100644
--- a/src/util/Backtrack_stack.mli
+++ b/src/util/Backtrack_stack.mli
@@ -19,3 +19,5 @@ val push_level : _ t -> unit
 
 val pop_levels : 'a t -> int -> f:('a -> unit) -> unit
 (** [pop_levels st n ~f] removes [n] levels, calling [f] on every removed item *)
+
+val iter : f:('a -> unit) -> 'a t -> unit
diff --git a/src/util/Profile.ml b/src/util/Profile.ml
new file mode 100644
index 00000000..c0d6b6ca
--- /dev/null
+++ b/src/util/Profile.ml
@@ -0,0 +1,102 @@
+
+module type BACKEND = sig
+  val get_ts : unit -> float
+
+  val emit_duration_event :
+    name : string ->
+    start : float ->
+    end_ : float ->
+    unit ->
+    unit
+
+  val emit_instant_event :
+    name : string ->
+    ts : float ->
+    unit ->
+    unit
+
+  val teardown : unit -> unit
+end
+
+type backend = (module BACKEND)
+
+type probe =
+  | No_probe
+  | Probe of {
+    name: string;
+    start: float;
+  }
+
+let null_probe = No_probe
+
+(* where to print events *)
+let out_ : backend option ref = ref None
+
+let begin_with_ (module B:BACKEND) name : probe =
+  Probe {name; start=B.get_ts ()}
+
+let[@inline] begin_ name : probe =
+  match !out_ with
+  | None -> No_probe
+  | Some b -> begin_with_ b name
+
+let[@inline] instant name =
+  match !out_ with
+  | None -> ()
+  | Some (module B) ->
+    let now = B.get_ts() in
+    B.emit_instant_event ~name ~ts:now ()
+
+(* slow path *)
+let exit_full_ (module B : BACKEND) name start =
+  let now = B.get_ts() in
+  B.emit_duration_event ~name ~start ~end_:now ()
+
+let exit_with_ b pb =
+  match pb with
+  | No_probe -> ()
+  | Probe {name; start} -> exit_full_ b name start
+
+let[@inline] exit pb =
+  match pb, !out_ with
+  | Probe {name;start}, Some b -> exit_full_ b name start
+  | _ -> ()
+
+let[@inline] with_ name f =
+  match !out_ with
+  | None -> f()
+  | Some b ->
+    let pb = begin_with_ b name in
+    try
+      let x = f() in
+      exit_with_ b pb;
+      x
+    with e ->
+      exit_with_ b pb;
+      raise e
+
+let[@inline] with1 name f x =
+  match !out_ with
+  | None -> f x
+  | Some b ->
+    let pb = begin_with_ b name in
+    try
+      let res = f x in
+      exit_with_ b pb;
+      res
+    with e ->
+      exit_with_ b pb;
+      raise e
+
+module Control = struct
+  let setup b =
+    assert (!out_ = None);
+    out_ := b
+
+  let teardown () =
+    match !out_ with
+    | None -> ()
+    | Some (module B) ->
+      out_ := None;
+      B.teardown()
+end
diff --git a/src/util/Profile.mli b/src/util/Profile.mli
new file mode 100644
index 00000000..ea3bb498
--- /dev/null
+++ b/src/util/Profile.mli
@@ -0,0 +1,43 @@
+
+(** {1 Profiling probes} *)
+
+type probe
+
+val null_probe : probe
+
+val instant : string -> unit
+
+val begin_ : string -> probe
+
+val exit : probe -> unit
+
+val with_ : string -> (unit -> 'a) -> 'a
+
+val with1 : string -> ('a -> 'b) -> 'a -> 'b
+
+module type BACKEND = sig
+  val get_ts : unit -> float
+
+  val emit_duration_event :
+    name : string ->
+    start : float ->
+    end_ : float ->
+    unit ->
+    unit
+
+  val emit_instant_event :
+    name : string ->
+    ts : float ->
+    unit ->
+    unit
+
+  val teardown : unit -> unit
+end
+
+type backend = (module BACKEND)
+
+module Control : sig
+  val setup : backend option -> unit
+
+  val teardown : unit -> unit
+end
diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml
index 710e65bf..53b0b2a3 100644
--- a/src/util/Sidekick_util.ml
+++ b/src/util/Sidekick_util.ml
@@ -12,3 +12,4 @@ module Intf = Intf
 module Bag = Bag
 module Stat = Stat
 module Hash = Hash
+module Profile = Profile
diff --git a/tests/sat/uart-10.induction.cvc.smt2 b/tests/sat/uart-10.induction.cvc.smt2
new file mode 100644
index 00000000..ba42a762
--- /dev/null
+++ b/tests/sat/uart-10.induction.cvc.smt2
@@ -0,0 +1,203 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_LRA)
+(set-info :source |
+Specification and verification of a 8N1 decoder.
+Geoffrey Brown, Indiana University <geobrown@cs.indiana.edu>
+Lee Pike, Galois Connections, Inc. <leepike@galois.com> 
+
+Translated into CVC format by Leonardo de Moura.
+
+This benchmark was automatically translated into SMT-LIB format from
+CVC format using CVC Lite
+
+
+
+|)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun x_0 () Real)
+(declare-fun x_1 () Real)
+(declare-fun x_2 () Real)
+(declare-fun x_3 () Real)
+(declare-fun x_4 () Real)
+(declare-fun x_5 () Real)
+(declare-fun x_6 () Real)
+(declare-fun x_7 () Real)
+(declare-fun x_8 () Real)
+(declare-fun x_9 () Real)
+(declare-fun x_10 () Bool)
+(declare-fun x_11 () Real)
+(declare-fun x_12 () Bool)
+(declare-fun x_13 () Real)
+(declare-fun x_14 () Bool)
+(declare-fun x_15 () Real)
+(declare-fun x_16 () Bool)
+(declare-fun x_17 () Real)
+(declare-fun x_18 () Bool)
+(declare-fun x_19 () Real)
+(declare-fun x_20 () Bool)
+(declare-fun x_21 () Real)
+(declare-fun x_22 () Bool)
+(declare-fun x_23 () Real)
+(declare-fun x_24 () Bool)
+(declare-fun x_25 () Real)
+(declare-fun x_26 () Bool)
+(declare-fun x_27 () Real)
+(declare-fun x_28 () Bool)
+(declare-fun x_29 () Real)
+(declare-fun x_30 () Bool)
+(declare-fun x_31 () Real)
+(declare-fun x_32 () Real)
+(declare-fun x_33 () Real)
+(declare-fun x_34 () Real)
+(declare-fun x_35 () Real)
+(declare-fun x_36 () Real)
+(declare-fun x_37 () Real)
+(declare-fun x_38 () Real)
+(declare-fun x_39 () Real)
+(declare-fun x_40 () Real)
+(declare-fun x_41 () Real)
+(declare-fun x_42 () Real)
+(declare-fun x_43 () Real)
+(declare-fun x_44 () Real)
+(declare-fun x_45 () Real)
+(declare-fun x_46 () Real)
+(declare-fun x_47 () Real)
+(declare-fun x_48 () Real)
+(declare-fun x_49 () Real)
+(declare-fun x_50 () Real)
+(declare-fun x_51 () Real)
+(declare-fun x_52 () Real)
+(declare-fun x_53 () Real)
+(declare-fun x_54 () Real)
+(declare-fun x_55 () Real)
+(declare-fun x_56 () Real)
+(declare-fun x_57 () Real)
+(declare-fun x_58 () Real)
+(declare-fun x_59 () Real)
+(declare-fun x_60 () Real)
+(declare-fun x_61 () Real)
+(declare-fun x_62 () Real)
+(declare-fun x_63 () Real)
+(declare-fun x_64 () Real)
+(declare-fun x_65 () Real)
+(declare-fun x_66 () Real)
+(declare-fun x_67 () Real)
+(declare-fun x_68 () Real)
+(declare-fun x_69 () Real)
+(declare-fun x_70 () Real)
+(declare-fun x_71 () Real)
+(declare-fun x_72 () Real)
+(declare-fun x_73 () Real)
+(declare-fun x_74 () Real)
+(declare-fun x_75 () Real)
+(declare-fun x_76 () Real)
+(declare-fun x_77 () Real)
+(declare-fun x_78 () Real)
+(declare-fun x_79 () Real)
+(declare-fun x_80 () Real)
+(declare-fun x_81 () Real)
+(declare-fun x_82 () Real)
+(declare-fun x_83 () Real)
+(declare-fun x_84 () Real)
+(declare-fun x_85 () Real)
+(declare-fun x_86 () Real)
+(declare-fun x_87 () Real)
+(declare-fun x_88 () Real)
+(declare-fun x_89 () Real)
+(declare-fun x_90 () Real)
+(declare-fun x_91 () Real)
+(declare-fun x_92 () Real)
+(declare-fun x_93 () Real)
+(declare-fun x_94 () Real)
+(declare-fun x_95 () Real)
+(declare-fun x_96 () Real)
+(declare-fun x_97 () Real)
+(declare-fun x_98 () Real)
+(declare-fun x_99 () Real)
+(declare-fun x_100 () Real)
+(declare-fun x_101 () Real)
+(declare-fun x_102 () Real)
+(declare-fun x_103 () Real)
+(declare-fun x_104 () Real)
+(declare-fun x_105 () Real)
+(declare-fun x_106 () Real)
+(declare-fun x_107 () Real)
+(declare-fun x_108 () Real)
+(declare-fun x_109 () Real)
+(declare-fun x_110 () Real)
+(declare-fun x_111 () Real)
+(declare-fun x_112 () Real)
+(declare-fun x_113 () Real)
+(declare-fun x_114 () Real)
+(declare-fun x_115 () Real)
+(declare-fun x_116 () Real)
+(declare-fun x_117 () Real)
+(declare-fun x_118 () Real)
+(declare-fun x_119 () Real)
+(declare-fun x_120 () Real)
+(declare-fun x_121 () Real)
+(declare-fun x_122 () Real)
+(declare-fun x_123 () Real)
+(declare-fun x_124 () Real)
+(declare-fun x_125 () Real)
+(declare-fun x_126 () Real)
+(declare-fun x_127 () Real)
+(declare-fun x_128 () Real)
+(declare-fun x_129 () Real)
+(declare-fun x_130 () Real)
+(declare-fun x_131 () Real)
+(declare-fun x_132 () Real)
+(declare-fun x_133 () Real)
+(declare-fun x_134 () Real)
+(declare-fun x_135 () Real)
+(declare-fun x_136 () Real)
+(declare-fun x_137 () Real)
+(declare-fun x_138 () Real)
+(declare-fun x_139 () Real)
+(declare-fun x_140 () Real)
+(declare-fun x_141 () Real)
+(declare-fun x_142 () Real)
+(declare-fun x_143 () Real)
+(declare-fun x_144 () Real)
+(declare-fun x_145 () Real)
+(declare-fun x_146 () Real)
+(declare-fun x_147 () Real)
+(declare-fun x_148 () Real)
+(declare-fun x_149 () Real)
+(declare-fun x_150 () Real)
+(declare-fun x_151 () Real)
+(declare-fun x_152 () Real)
+(declare-fun x_153 () Real)
+(declare-fun x_154 () Real)
+(declare-fun x_155 () Real)
+(declare-fun x_156 () Real)
+(declare-fun x_157 () Real)
+(declare-fun x_158 () Real)
+(declare-fun x_159 () Real)
+(declare-fun x_160 () Real)
+(declare-fun x_161 () Real)
+(declare-fun x_162 () Real)
+(declare-fun x_163 () Real)
+(declare-fun x_164 () Real)
+(declare-fun x_165 () Real)
+(declare-fun x_166 () Real)
+(declare-fun x_167 () Real)
+(declare-fun x_168 () Real)
+(declare-fun x_169 () Real)
+(declare-fun x_170 () Real)
+(declare-fun x_171 () Real)
+(declare-fun x_172 () Real)
+(declare-fun x_173 () Real)
+(declare-fun x_174 () Real)
+(declare-fun x_175 () Real)
+(declare-fun x_176 () Real)
+(declare-fun x_177 () Real)
+(declare-fun x_178 () Real)
+(declare-fun x_179 () Real)
+(declare-fun x_180 () Real)
+(declare-fun x_181 () Real)
+(declare-fun x_182 () Real)
+(assert (let ((?v_14 (not x_28))) (let ((?v_16 (and ?v_14 (< x_29 8))) (?v_57 (not x_26))) (let ((?v_59 (and ?v_57 (< x_27 8))) (?v_95 (not x_24))) (let ((?v_97 (and ?v_95 (< x_25 8))) (?v_133 (not x_22))) (let ((?v_135 (and ?v_133 (< x_23 8))) (?v_171 (not x_20))) (let ((?v_173 (and ?v_171 (< x_21 8))) (?v_209 (not x_18))) (let ((?v_211 (and ?v_209 (< x_19 8))) (?v_247 (not x_16))) (let ((?v_249 (and ?v_247 (< x_17 8))) (?v_285 (not x_14))) (let ((?v_287 (and ?v_285 (< x_15 8))) (?v_323 (not x_12))) (let ((?v_325 (and ?v_323 (< x_13 8))) (?v_361 (not x_10))) (let ((?v_363 (and ?v_361 (< x_11 8))) (?v_351 (= x_32 10)) (?v_353 (= x_33 1)) (?v_355 (= x_12 x_10)) (?v_356 (= x_34 x_35)) (?v_360 (= x_36 x_35)) (?v_357 (= x_37 x_38)) (?v_359 (= x_39 x_40)) (?v_364 (= x_11 9)) (?v_365 (= x_37 1)) (?v_366 (not (= x_40 1))) (?v_367 (not (= x_40 0))) (?v_368 (= x_40 3)) (?v_369 (= x_40 2)) (?v_358 (= x_13 x_11)) (?v_370 (= x_41 x_36)) (?v_349 (= x_42 x_43)) (?v_371 (= x_33 x_44)) (?v_350 (= x_45 x_32)) (?v_372 (= x_46 x_47)) (?v_373 (< x_32 9)) (?v_375 (= x_0 2)) (?v_374 (= x_36 x_47)) (?v_379 (= x_35 x_36))) (let ((?v_380 (not ?v_379)) (?v_377 (= x_11 x_32)) (?v_385 (not (= x_43 x_38))) (?v_344 (= x_1 1)) (?v_313 (= x_45 10)) (?v_315 (= x_56 1)) (?v_317 (= x_14 x_12)) (?v_318 (= x_57 x_34)) (?v_322 (= x_41 x_34)) (?v_319 (= x_58 x_37)) (?v_321 (= x_59 x_39)) (?v_326 (= x_13 9)) (?v_327 (= x_58 1)) (?v_328 (not (= x_39 1))) (?v_329 (not (= x_39 0))) (?v_330 (= x_39 3)) (?v_331 (= x_39 2)) (?v_320 (= x_15 x_13)) (?v_332 (= x_60 x_41)) (?v_311 (= x_61 x_42)) (?v_333 (= x_56 x_33)) (?v_312 (= x_62 x_45)) (?v_334 (= x_63 x_46)) (?v_335 (< x_45 9)) (?v_337 (= x_1 2)) (?v_336 (= x_41 x_46)) (?v_341 (= x_34 x_41))) (let ((?v_342 (not ?v_341)) (?v_339 (= x_13 x_45)) (?v_347 (not (= x_42 x_37))) (?v_306 (= x_2 1)) (?v_275 (= x_62 10)) (?v_277 (= x_70 1)) (?v_279 (= x_16 x_14)) (?v_280 (= x_71 x_57)) (?v_284 (= x_60 x_57)) (?v_281 (= x_72 x_58)) (?v_283 (= x_73 x_59)) (?v_288 (= x_15 9)) (?v_289 (= x_72 1)) (?v_290 (not (= x_59 1))) (?v_291 (not (= x_59 0))) (?v_292 (= x_59 3)) (?v_293 (= x_59 2)) (?v_282 (= x_17 x_15)) (?v_294 (= x_74 x_60)) (?v_273 (= x_75 x_61)) (?v_295 (= x_70 x_56)) (?v_274 (= x_76 x_62)) (?v_296 (= x_77 x_63)) (?v_297 (< x_62 9)) (?v_299 (= x_2 2)) (?v_298 (= x_60 x_63)) (?v_303 (= x_57 x_60))) (let ((?v_304 (not ?v_303)) (?v_301 (= x_15 x_62)) (?v_309 (not (= x_61 x_58))) (?v_268 (= x_3 1)) (?v_237 (= x_76 10)) (?v_239 (= x_84 1)) (?v_241 (= x_18 x_16)) (?v_242 (= x_85 x_71)) (?v_246 (= x_74 x_71)) (?v_243 (= x_86 x_72)) (?v_245 (= x_87 x_73)) (?v_250 (= x_17 9)) (?v_251 (= x_86 1)) (?v_252 (not (= x_73 1))) (?v_253 (not (= x_73 0))) (?v_254 (= x_73 3)) (?v_255 (= x_73 2)) (?v_244 (= x_19 x_17)) (?v_256 (= x_88 x_74)) (?v_235 (= x_89 x_75)) (?v_257 (= x_84 x_70)) (?v_236 (= x_90 x_76)) (?v_258 (= x_91 x_77)) (?v_259 (< x_76 9)) (?v_261 (= x_3 2)) (?v_260 (= x_74 x_77)) (?v_265 (= x_71 x_74))) (let ((?v_266 (not ?v_265)) (?v_263 (= x_17 x_76)) (?v_271 (not (= x_75 x_72))) (?v_230 (= x_4 1)) (?v_199 (= x_90 10)) (?v_201 (= x_98 1)) (?v_203 (= x_20 x_18)) (?v_204 (= x_99 x_85)) (?v_208 (= x_88 x_85)) (?v_205 (= x_100 x_86)) (?v_207 (= x_101 x_87)) (?v_212 (= x_19 9)) (?v_213 (= x_100 1)) (?v_214 (not (= x_87 1))) (?v_215 (not (= x_87 0))) (?v_216 (= x_87 3)) (?v_217 (= x_87 2)) (?v_206 (= x_21 x_19)) (?v_218 (= x_102 x_88)) (?v_197 (= x_103 x_89)) (?v_219 (= x_98 x_84)) (?v_198 (= x_104 x_90)) (?v_220 (= x_105 x_91)) (?v_221 (< x_90 9)) (?v_223 (= x_4 2)) (?v_222 (= x_88 x_91)) (?v_227 (= x_85 x_88))) (let ((?v_228 (not ?v_227)) (?v_225 (= x_19 x_90)) (?v_233 (not (= x_89 x_86))) (?v_192 (= x_5 1)) (?v_161 (= x_104 10)) (?v_163 (= x_112 1)) (?v_165 (= x_22 x_20)) (?v_166 (= x_113 x_99)) (?v_170 (= x_102 x_99)) (?v_167 (= x_114 x_100)) (?v_169 (= x_115 x_101)) (?v_174 (= x_21 9)) (?v_175 (= x_114 1)) (?v_176 (not (= x_101 1))) (?v_177 (not (= x_101 0))) (?v_178 (= x_101 3)) (?v_179 (= x_101 2)) (?v_168 (= x_23 x_21)) (?v_180 (= x_116 x_102)) (?v_159 (= x_117 x_103)) (?v_181 (= x_112 x_98)) (?v_160 (= x_118 x_104)) (?v_182 (= x_119 x_105)) (?v_183 (< x_104 9)) (?v_185 (= x_5 2)) (?v_184 (= x_102 x_105)) (?v_189 (= x_99 x_102))) (let ((?v_190 (not ?v_189)) (?v_187 (= x_21 x_104)) (?v_195 (not (= x_103 x_100))) (?v_154 (= x_6 1)) (?v_123 (= x_118 10)) (?v_125 (= x_126 1)) (?v_127 (= x_24 x_22)) (?v_128 (= x_127 x_113)) (?v_132 (= x_116 x_113)) (?v_129 (= x_128 x_114)) (?v_131 (= x_129 x_115)) (?v_136 (= x_23 9)) (?v_137 (= x_128 1)) (?v_138 (not (= x_115 1))) (?v_139 (not (= x_115 0))) (?v_140 (= x_115 3)) (?v_141 (= x_115 2)) (?v_130 (= x_25 x_23)) (?v_142 (= x_130 x_116)) (?v_121 (= x_131 x_117)) (?v_143 (= x_126 x_112)) (?v_122 (= x_132 x_118)) (?v_144 (= x_133 x_119)) (?v_145 (< x_118 9)) (?v_147 (= x_6 2)) (?v_146 (= x_116 x_119)) (?v_151 (= x_113 x_116))) (let ((?v_152 (not ?v_151)) (?v_149 (= x_23 x_118)) (?v_157 (not (= x_117 x_114))) (?v_116 (= x_7 1)) (?v_85 (= x_132 10)) (?v_87 (= x_140 1)) (?v_89 (= x_26 x_24)) (?v_90 (= x_141 x_127)) (?v_94 (= x_130 x_127)) (?v_91 (= x_142 x_128)) (?v_93 (= x_143 x_129)) (?v_98 (= x_25 9)) (?v_99 (= x_142 1)) (?v_100 (not (= x_129 1))) (?v_101 (not (= x_129 0))) (?v_102 (= x_129 3)) (?v_103 (= x_129 2)) (?v_92 (= x_27 x_25)) (?v_104 (= x_144 x_130)) (?v_83 (= x_145 x_131)) (?v_105 (= x_140 x_126)) (?v_84 (= x_146 x_132)) (?v_106 (= x_147 x_133)) (?v_107 (< x_132 9)) (?v_109 (= x_7 2)) (?v_108 (= x_130 x_133)) (?v_113 (= x_127 x_130))) (let ((?v_114 (not ?v_113)) (?v_111 (= x_25 x_132)) (?v_119 (not (= x_131 x_128))) (?v_78 (= x_8 1)) (?v_42 (= x_146 10)) (?v_44 (= x_154 1)) (?v_50 (= x_28 x_26)) (?v_51 (= x_155 x_141)) (?v_55 (= x_144 x_141)) (?v_52 (= x_156 x_142)) (?v_54 (= x_157 x_143)) (?v_60 (= x_27 9)) (?v_61 (= x_156 1)) (?v_62 (not (= x_143 1))) (?v_63 (not (= x_143 0))) (?v_64 (= x_143 3)) (?v_65 (= x_143 2)) (?v_53 (= x_29 x_27)) (?v_66 (= x_158 x_144)) (?v_40 (= x_159 x_145)) (?v_67 (= x_154 x_140)) (?v_41 (= x_160 x_146)) (?v_68 (= x_161 x_147)) (?v_69 (< x_146 9)) (?v_71 (= x_8 2)) (?v_70 (= x_144 x_147)) (?v_75 (= x_141 x_144))) (let ((?v_76 (not ?v_75)) (?v_73 (= x_27 x_146)) (?v_81 (not (= x_145 x_142))) (?v_34 (= x_9 1)) (?v_2 (= x_160 10)) (?v_4 (= x_168 1)) (?v_8 (= x_30 x_28)) (?v_9 (= x_169 x_155)) (?v_13 (= x_158 x_155)) (?v_10 (= x_170 x_156)) (?v_12 (= x_171 x_157)) (?v_17 (= x_29 9)) (?v_18 (= x_170 1)) (?v_19 (not (= x_157 1))) (?v_20 (not (= x_157 0))) (?v_21 (= x_157 3)) (?v_22 (= x_157 2)) (?v_11 (= x_31 x_29)) (?v_23 (= x_172 x_158)) (?v_0 (= x_173 x_159)) (?v_24 (= x_168 x_154)) (?v_1 (= x_174 x_160)) (?v_25 (= x_175 x_161)) (?v_26 (< x_160 9)) (?v_28 (= x_9 2)) (?v_27 (= x_158 x_161)) (?v_32 (= x_155 x_158))) (let ((?v_33 (not ?v_32)) (?v_30 (= x_29 x_160)) (?v_38 (not (= x_159 x_156))) (?v_35 (= x_176 1)) (?v_362 (not (< x_37 0))) (?v_324 (not (< x_58 0))) (?v_286 (not (< x_72 0))) (?v_248 (not (< x_86 0))) (?v_210 (not (< x_100 0))) (?v_172 (not (< x_114 0))) (?v_134 (not (< x_128 0))) (?v_96 (not (< x_142 0))) (?v_58 (not (< x_156 0))) (?v_15 (not (< x_170 0))) (?v_382 (= x_0 1)) (?v_3 (= x_168 0)) (?v_5 (= x_174 1)) (?v_77 (= x_9 0)) (?v_43 (= x_154 0)) (?v_45 (= x_160 1)) (?v_115 (= x_8 0)) (?v_86 (= x_140 0)) (?v_88 (= x_146 1)) (?v_153 (= x_7 0)) (?v_124 (= x_126 0)) (?v_126 (= x_132 1)) (?v_191 (= x_6 0)) (?v_162 (= x_112 0)) (?v_164 (= x_118 1)) (?v_229 (= x_5 0)) (?v_200 (= x_98 0)) (?v_202 (= x_104 1)) (?v_267 (= x_4 0)) (?v_238 (= x_84 0)) (?v_240 (= x_90 1)) (?v_305 (= x_3 0)) (?v_276 (= x_70 0)) (?v_278 (= x_76 1)) (?v_343 (= x_2 0)) (?v_314 (= x_56 0)) (?v_316 (= x_62 1)) (?v_381 (= x_1 0)) (?v_352 (= x_33 0)) (?v_354 (= x_45 1)) (?v_36 (not ?v_26)) (?v_37 (and ?v_26 (not ?v_27))) (?v_31 (and ?v_26 ?v_27))) (let ((?v_29 (and ?v_31 ?v_33))) (let ((?v_39 (and ?v_29 ?v_30)) (?v_79 (not ?v_69)) (?v_80 (and ?v_69 (not ?v_70))) (?v_74 (and ?v_69 ?v_70))) (let ((?v_72 (and ?v_74 ?v_76))) (let ((?v_82 (and ?v_72 ?v_73)) (?v_117 (not ?v_107)) (?v_118 (and ?v_107 (not ?v_108))) (?v_112 (and ?v_107 ?v_108))) (let ((?v_110 (and ?v_112 ?v_114))) (let ((?v_120 (and ?v_110 ?v_111)) (?v_155 (not ?v_145)) (?v_156 (and ?v_145 (not ?v_146))) (?v_150 (and ?v_145 ?v_146))) (let ((?v_148 (and ?v_150 ?v_152))) (let ((?v_158 (and ?v_148 ?v_149)) (?v_193 (not ?v_183)) (?v_194 (and ?v_183 (not ?v_184))) (?v_188 (and ?v_183 ?v_184))) (let ((?v_186 (and ?v_188 ?v_190))) (let ((?v_196 (and ?v_186 ?v_187)) (?v_231 (not ?v_221)) (?v_232 (and ?v_221 (not ?v_222))) (?v_226 (and ?v_221 ?v_222))) (let ((?v_224 (and ?v_226 ?v_228))) (let ((?v_234 (and ?v_224 ?v_225)) (?v_269 (not ?v_259)) (?v_270 (and ?v_259 (not ?v_260))) (?v_264 (and ?v_259 ?v_260))) (let ((?v_262 (and ?v_264 ?v_266))) (let ((?v_272 (and ?v_262 ?v_263)) (?v_307 (not ?v_297)) (?v_308 (and ?v_297 (not ?v_298))) (?v_302 (and ?v_297 ?v_298))) (let ((?v_300 (and ?v_302 ?v_304))) (let ((?v_310 (and ?v_300 ?v_301)) (?v_345 (not ?v_335)) (?v_346 (and ?v_335 (not ?v_336))) (?v_340 (and ?v_335 ?v_336))) (let ((?v_338 (and ?v_340 ?v_342))) (let ((?v_348 (and ?v_338 ?v_339)) (?v_383 (not ?v_373)) (?v_384 (and ?v_373 (not ?v_374))) (?v_378 (and ?v_373 ?v_374))) (let ((?v_376 (and ?v_378 ?v_380))) (let ((?v_386 (and ?v_376 ?v_377)) (?v_6 (- 1 x_51))) (let ((?v_46 (* ?v_6 23)) (?v_7 (+ x_51 1))) (let ((?v_47 (* ?v_7 23)) (?v_48 (* ?v_6 16)) (?v_49 (* ?v_7 16)) (?v_56 (- 16 x_53))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_171 3) (>= x_171 0)) (<= x_168 3)) (>= x_168 0)) (<= x_157 3)) (>= x_157 0)) (<= x_154 3)) (>= x_154 0)) (<= x_143 3)) (>= x_143 0)) (<= x_140 3)) (>= x_140 0)) (<= x_129 3)) (>= x_129 0)) (<= x_126 3)) (>= x_126 0)) (<= x_115 3)) (>= x_115 0)) (<= x_112 3)) (>= x_112 0)) (<= x_101 3)) (>= x_101 0)) (<= x_98 3)) (>= x_98 0)) (<= x_87 3)) (>= x_87 0)) (<= x_84 3)) (>= x_84 0)) (<= x_73 3)) (>= x_73 0)) (<= x_70 3)) (>= x_70 0)) (<= x_59 3)) (>= x_59 0)) (<= x_56 3)) (>= x_56 0)) (<= x_44 3)) (>= x_44 0)) (<= x_40 3)) (>= x_40 0)) (<= x_39 3)) (>= x_39 0)) (<= x_33 3)) (>= x_33 0)) (not (< x_0 0))) (<= x_0 2)) (not (< x_1 0))) (<= x_1 2)) (not (< x_2 0))) (<= x_2 2)) (not (< x_3 0))) (<= x_3 2)) (not (< x_4 0))) (<= x_4 2)) (not (< x_5 0))) (<= x_5 2)) (not (< x_6 0))) (<= x_6 2)) (not (< x_7 0))) (<= x_7 2)) (not (< x_8 0))) (<= x_8 2)) (not (< x_9 0))) (<= x_9 2)) (not (< x_11 0))) (<= x_11 9)) (not (< x_13 0))) (<= x_13 9)) (not (< x_15 0))) (<= x_15 9)) (not (< x_17 0))) (<= x_17 9)) (not (< x_19 0))) (<= x_19 9)) (not (< x_21 0))) (<= x_21 9)) (not (< x_23 0))) (<= x_23 9)) (not (< x_25 0))) (<= x_25 9)) (not (< x_27 0))) (<= x_27 9)) (not (< x_29 0))) (<= x_29 9)) (not (< x_31 0))) (<= x_31 9)) (not (< x_32 1))) (<= x_32 10)) ?v_362) (<= x_37 1)) (not (< x_38 0))) (<= x_38 1)) (not (< x_42 0))) (<= x_42 1)) (not (< x_43 0))) (<= x_43 1)) (not (< x_45 1))) (<= x_45 10)) (>= x_51 0)) (< x_51 (/ 3 151))) (>= x_53 0)) (< x_53 4)) ?v_324) (<= x_58 1)) (not (< x_61 0))) (<= x_61 1)) (not (< x_62 1))) (<= x_62 10)) ?v_286) (<= x_72 1)) (not (< x_75 0))) (<= x_75 1)) (not (< x_76 1))) (<= x_76 10)) ?v_248) (<= x_86 1)) (not (< x_89 0))) (<= x_89 1)) (not (< x_90 1))) (<= x_90 10)) ?v_210) (<= x_100 1)) (not (< x_103 0))) (<= x_103 1)) (not (< x_104 1))) (<= x_104 10)) ?v_172) (<= x_114 1)) (not (< x_117 0))) (<= x_117 1)) (not (< x_118 1))) (<= x_118 10)) ?v_134) (<= x_128 1)) (not (< x_131 0))) (<= x_131 1)) (not (< x_132 1))) (<= x_132 10)) ?v_96) (<= x_142 1)) (not (< x_145 0))) (<= x_145 1)) (not (< x_146 1))) (<= x_146 10)) ?v_58) (<= x_156 1)) (not (< x_159 0))) (<= x_159 1)) (not (< x_160 1))) (<= x_160 10)) ?v_15) (<= x_170 1)) (not (< x_173 0))) (<= x_173 1)) (not (< x_174 1))) (<= x_174 10)) (not (< x_176 0))) (<= x_176 2)) (not ?v_34)) (not ?v_78)) (not ?v_116)) (not ?v_154)) (not ?v_192)) (not ?v_230)) (not ?v_268)) (not ?v_306)) (not ?v_344)) (not ?v_382)) (or (or (and (and (and (and (and (and (and (and (and (and (= x_177 0) (or (and (and (and (= x_178 0) (< x_158 x_161)) (<= x_161 x_155)) (= x_172 x_161)) (and (and (and (= x_178 1) (< x_158 x_155)) (<= x_155 x_161)) (= x_172 x_155)))) ?v_0) ?v_24) ?v_1) ?v_25) ?v_8) ?v_9) ?v_10) ?v_11) ?v_12) (and (and (and (and (and (and (and (and (and (= x_177 1) (or (or (and (and (and (and (and (= x_179 0) ?v_2) ?v_20) ?v_4) ?v_0) ?v_1) (and (and (and (and (and (= x_179 1) ?v_2) ?v_19) ?v_3) ?v_5) ?v_0)) (and (and (and (and (= x_179 2) (not ?v_2)) (ite (or ?v_22 ?v_21) (or ?v_3 ?v_4) (= x_168 x_157))) (= x_174 (+ x_160 1))) (= x_173 (ite ?v_4 1 0))))) ?v_27) (ite (= x_174 10) (and (<= (+ x_158 ?v_6) x_175) (<= x_175 (+ (+ x_158 x_51) 1))) (ite ?v_5 (and (<= (+ x_158 ?v_46) x_175) (<= x_175 (+ x_158 ?v_47))) (and (<= (+ x_158 ?v_48) x_175) (<= x_175 (+ x_158 ?v_49)))))) ?v_23) ?v_8) ?v_9) ?v_10) ?v_11) ?v_12)) (and (and (and (and (and (and (and (and (= x_177 2) (or (and (and (and (and (= x_180 0) ?v_13) ?v_14) (= x_169 (+ x_158 x_53))) x_30) (and (and (and (and (= x_180 1) ?v_13) x_28) (= x_169 (+ x_158 ?v_56))) (not x_30)))) (or (and (and (and (= x_181 0) ?v_16) (or (= x_170 0) ?v_18)) ?v_15) (and (and (= x_181 1) (not ?v_16)) ?v_10))) (or (or (or (and (and (and (and (= x_182 0) ?v_14) ?v_17) (= x_31 9)) ?v_12) (and (and (and (and (= x_182 1) ?v_14) ?v_17) (= x_171 2)) (= x_31 0))) (and (and (and (and (= x_182 2) ?v_14) (< x_29 9)) (= x_171 (ite (or ?v_18 (= x_29 8)) (ite ?v_19 3 x_157) (ite ?v_20 2 x_157)))) (= x_31 (+ x_29 1)))) (and (and (and (= x_182 3) x_28) (= x_171 (ite ?v_21 1 (ite ?v_22 0 x_157)))) ?v_11))) ?v_23) ?v_0) ?v_24) ?v_1) ?v_25))) (or (or (or (or (and (and ?v_28 (or (or ?v_36 ?v_37) ?v_39)) (= x_176 2)) (and (and ?v_28 (or (and ?v_29 (not ?v_30)) (and ?v_31 ?v_32))) ?v_35)) (and (and (and (and (and ?v_28 ?v_26) ?v_27) ?v_33) ?v_30) (= x_176 0))) (and ?v_34 ?v_35)) (and (and ?v_77 (or (or (and ?v_36 ?v_38) (and ?v_37 ?v_38)) (and ?v_39 ?v_38))) ?v_35))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_162 0) (or (and (and (and (= x_163 0) (< x_144 x_147)) (<= x_147 x_141)) (= x_158 x_147)) (and (and (and (= x_163 1) (< x_144 x_141)) (<= x_141 x_147)) (= x_158 x_141)))) ?v_40) ?v_67) ?v_41) ?v_68) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) (and (and (and (and (and (and (and (and (and (= x_162 1) (or (or (and (and (and (and (and (= x_164 0) ?v_42) ?v_63) ?v_44) ?v_40) ?v_41) (and (and (and (and (and (= x_164 1) ?v_42) ?v_62) ?v_43) ?v_45) ?v_40)) (and (and (and (and (= x_164 2) (not ?v_42)) (ite (or ?v_65 ?v_64) (or ?v_43 ?v_44) (= x_154 x_143))) (= x_160 (+ x_146 1))) (= x_159 (ite ?v_44 1 0))))) ?v_70) (ite ?v_2 (and (<= (+ x_144 ?v_6) x_161) (<= x_161 (+ (+ x_144 x_51) 1))) (ite ?v_45 (and (<= (+ x_144 ?v_46) x_161) (<= x_161 (+ x_144 ?v_47))) (and (<= (+ x_144 ?v_48) x_161) (<= x_161 (+ x_144 ?v_49)))))) ?v_66) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54)) (and (and (and (and (and (and (and (and (= x_162 2) (or (and (and (and (and (= x_165 0) ?v_55) ?v_57) (= x_155 (+ x_144 x_53))) x_28) (and (and (and (and (= x_165 1) ?v_55) x_26) (= x_155 (+ x_144 ?v_56))) ?v_14))) (or (and (and (and (= x_166 0) ?v_59) (or (= x_156 0) ?v_61)) ?v_58) (and (and (= x_166 1) (not ?v_59)) ?v_52))) (or (or (or (and (and (and (and (= x_167 0) ?v_57) ?v_60) ?v_17) ?v_54) (and (and (and (and (= x_167 1) ?v_57) ?v_60) ?v_22) (= x_29 0))) (and (and (and (and (= x_167 2) ?v_57) (< x_27 9)) (= x_157 (ite (or ?v_61 (= x_27 8)) (ite ?v_62 3 x_143) (ite ?v_63 2 x_143)))) (= x_29 (+ x_27 1)))) (and (and (and (= x_167 3) x_26) (= x_157 (ite ?v_64 1 (ite ?v_65 0 x_143)))) ?v_53))) ?v_66) ?v_40) ?v_67) ?v_41) ?v_68))) (or (or (or (or (and (and ?v_71 (or (or ?v_79 ?v_80) ?v_82)) ?v_28) (and (and ?v_71 (or (and ?v_72 (not ?v_73)) (and ?v_74 ?v_75))) ?v_34)) (and (and (and (and (and ?v_71 ?v_69) ?v_70) ?v_76) ?v_73) ?v_77)) (and ?v_78 ?v_34)) (and (and ?v_115 (or (or (and ?v_79 ?v_81) (and ?v_80 ?v_81)) (and ?v_82 ?v_81))) ?v_34))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_148 0) (or (and (and (and (= x_149 0) (< x_130 x_133)) (<= x_133 x_127)) (= x_144 x_133)) (and (and (and (= x_149 1) (< x_130 x_127)) (<= x_127 x_133)) (= x_144 x_127)))) ?v_83) ?v_105) ?v_84) ?v_106) ?v_89) ?v_90) ?v_91) ?v_92) ?v_93) (and (and (and (and (and (and (and (and (and (= x_148 1) (or (or (and (and (and (and (and (= x_150 0) ?v_85) ?v_101) ?v_87) ?v_83) ?v_84) (and (and (and (and (and (= x_150 1) ?v_85) ?v_100) ?v_86) ?v_88) ?v_83)) (and (and (and (and (= x_150 2) (not ?v_85)) (ite (or ?v_103 ?v_102) (or ?v_86 ?v_87) (= x_140 x_129))) (= x_146 (+ x_132 1))) (= x_145 (ite ?v_87 1 0))))) ?v_108) (ite ?v_42 (and (<= (+ x_130 ?v_6) x_147) (<= x_147 (+ (+ x_130 x_51) 1))) (ite ?v_88 (and (<= (+ x_130 ?v_46) x_147) (<= x_147 (+ x_130 ?v_47))) (and (<= (+ x_130 ?v_48) x_147) (<= x_147 (+ x_130 ?v_49)))))) ?v_104) ?v_89) ?v_90) ?v_91) ?v_92) ?v_93)) (and (and (and (and (and (and (and (and (= x_148 2) (or (and (and (and (and (= x_151 0) ?v_94) ?v_95) (= x_141 (+ x_130 x_53))) x_26) (and (and (and (and (= x_151 1) ?v_94) x_24) (= x_141 (+ x_130 ?v_56))) ?v_57))) (or (and (and (and (= x_152 0) ?v_97) (or (= x_142 0) ?v_99)) ?v_96) (and (and (= x_152 1) (not ?v_97)) ?v_91))) (or (or (or (and (and (and (and (= x_153 0) ?v_95) ?v_98) ?v_60) ?v_93) (and (and (and (and (= x_153 1) ?v_95) ?v_98) ?v_65) (= x_27 0))) (and (and (and (and (= x_153 2) ?v_95) (< x_25 9)) (= x_143 (ite (or ?v_99 (= x_25 8)) (ite ?v_100 3 x_129) (ite ?v_101 2 x_129)))) (= x_27 (+ x_25 1)))) (and (and (and (= x_153 3) x_24) (= x_143 (ite ?v_102 1 (ite ?v_103 0 x_129)))) ?v_92))) ?v_104) ?v_83) ?v_105) ?v_84) ?v_106))) (or (or (or (or (and (and ?v_109 (or (or ?v_117 ?v_118) ?v_120)) ?v_71) (and (and ?v_109 (or (and ?v_110 (not ?v_111)) (and ?v_112 ?v_113))) ?v_78)) (and (and (and (and (and ?v_109 ?v_107) ?v_108) ?v_114) ?v_111) ?v_115)) (and ?v_116 ?v_78)) (and (and ?v_153 (or (or (and ?v_117 ?v_119) (and ?v_118 ?v_119)) (and ?v_120 ?v_119))) ?v_78))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_134 0) (or (and (and (and (= x_135 0) (< x_116 x_119)) (<= x_119 x_113)) (= x_130 x_119)) (and (and (and (= x_135 1) (< x_116 x_113)) (<= x_113 x_119)) (= x_130 x_113)))) ?v_121) ?v_143) ?v_122) ?v_144) ?v_127) ?v_128) ?v_129) ?v_130) ?v_131) (and (and (and (and (and (and (and (and (and (= x_134 1) (or (or (and (and (and (and (and (= x_136 0) ?v_123) ?v_139) ?v_125) ?v_121) ?v_122) (and (and (and (and (and (= x_136 1) ?v_123) ?v_138) ?v_124) ?v_126) ?v_121)) (and (and (and (and (= x_136 2) (not ?v_123)) (ite (or ?v_141 ?v_140) (or ?v_124 ?v_125) (= x_126 x_115))) (= x_132 (+ x_118 1))) (= x_131 (ite ?v_125 1 0))))) ?v_146) (ite ?v_85 (and (<= (+ x_116 ?v_6) x_133) (<= x_133 (+ (+ x_116 x_51) 1))) (ite ?v_126 (and (<= (+ x_116 ?v_46) x_133) (<= x_133 (+ x_116 ?v_47))) (and (<= (+ x_116 ?v_48) x_133) (<= x_133 (+ x_116 ?v_49)))))) ?v_142) ?v_127) ?v_128) ?v_129) ?v_130) ?v_131)) (and (and (and (and (and (and (and (and (= x_134 2) (or (and (and (and (and (= x_137 0) ?v_132) ?v_133) (= x_127 (+ x_116 x_53))) x_24) (and (and (and (and (= x_137 1) ?v_132) x_22) (= x_127 (+ x_116 ?v_56))) ?v_95))) (or (and (and (and (= x_138 0) ?v_135) (or (= x_128 0) ?v_137)) ?v_134) (and (and (= x_138 1) (not ?v_135)) ?v_129))) (or (or (or (and (and (and (and (= x_139 0) ?v_133) ?v_136) ?v_98) ?v_131) (and (and (and (and (= x_139 1) ?v_133) ?v_136) ?v_103) (= x_25 0))) (and (and (and (and (= x_139 2) ?v_133) (< x_23 9)) (= x_129 (ite (or ?v_137 (= x_23 8)) (ite ?v_138 3 x_115) (ite ?v_139 2 x_115)))) (= x_25 (+ x_23 1)))) (and (and (and (= x_139 3) x_22) (= x_129 (ite ?v_140 1 (ite ?v_141 0 x_115)))) ?v_130))) ?v_142) ?v_121) ?v_143) ?v_122) ?v_144))) (or (or (or (or (and (and ?v_147 (or (or ?v_155 ?v_156) ?v_158)) ?v_109) (and (and ?v_147 (or (and ?v_148 (not ?v_149)) (and ?v_150 ?v_151))) ?v_116)) (and (and (and (and (and ?v_147 ?v_145) ?v_146) ?v_152) ?v_149) ?v_153)) (and ?v_154 ?v_116)) (and (and ?v_191 (or (or (and ?v_155 ?v_157) (and ?v_156 ?v_157)) (and ?v_158 ?v_157))) ?v_116))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_120 0) (or (and (and (and (= x_121 0) (< x_102 x_105)) (<= x_105 x_99)) (= x_116 x_105)) (and (and (and (= x_121 1) (< x_102 x_99)) (<= x_99 x_105)) (= x_116 x_99)))) ?v_159) ?v_181) ?v_160) ?v_182) ?v_165) ?v_166) ?v_167) ?v_168) ?v_169) (and (and (and (and (and (and (and (and (and (= x_120 1) (or (or (and (and (and (and (and (= x_122 0) ?v_161) ?v_177) ?v_163) ?v_159) ?v_160) (and (and (and (and (and (= x_122 1) ?v_161) ?v_176) ?v_162) ?v_164) ?v_159)) (and (and (and (and (= x_122 2) (not ?v_161)) (ite (or ?v_179 ?v_178) (or ?v_162 ?v_163) (= x_112 x_101))) (= x_118 (+ x_104 1))) (= x_117 (ite ?v_163 1 0))))) ?v_184) (ite ?v_123 (and (<= (+ x_102 ?v_6) x_119) (<= x_119 (+ (+ x_102 x_51) 1))) (ite ?v_164 (and (<= (+ x_102 ?v_46) x_119) (<= x_119 (+ x_102 ?v_47))) (and (<= (+ x_102 ?v_48) x_119) (<= x_119 (+ x_102 ?v_49)))))) ?v_180) ?v_165) ?v_166) ?v_167) ?v_168) ?v_169)) (and (and (and (and (and (and (and (and (= x_120 2) (or (and (and (and (and (= x_123 0) ?v_170) ?v_171) (= x_113 (+ x_102 x_53))) x_22) (and (and (and (and (= x_123 1) ?v_170) x_20) (= x_113 (+ x_102 ?v_56))) ?v_133))) (or (and (and (and (= x_124 0) ?v_173) (or (= x_114 0) ?v_175)) ?v_172) (and (and (= x_124 1) (not ?v_173)) ?v_167))) (or (or (or (and (and (and (and (= x_125 0) ?v_171) ?v_174) ?v_136) ?v_169) (and (and (and (and (= x_125 1) ?v_171) ?v_174) ?v_141) (= x_23 0))) (and (and (and (and (= x_125 2) ?v_171) (< x_21 9)) (= x_115 (ite (or ?v_175 (= x_21 8)) (ite ?v_176 3 x_101) (ite ?v_177 2 x_101)))) (= x_23 (+ x_21 1)))) (and (and (and (= x_125 3) x_20) (= x_115 (ite ?v_178 1 (ite ?v_179 0 x_101)))) ?v_168))) ?v_180) ?v_159) ?v_181) ?v_160) ?v_182))) (or (or (or (or (and (and ?v_185 (or (or ?v_193 ?v_194) ?v_196)) ?v_147) (and (and ?v_185 (or (and ?v_186 (not ?v_187)) (and ?v_188 ?v_189))) ?v_154)) (and (and (and (and (and ?v_185 ?v_183) ?v_184) ?v_190) ?v_187) ?v_191)) (and ?v_192 ?v_154)) (and (and ?v_229 (or (or (and ?v_193 ?v_195) (and ?v_194 ?v_195)) (and ?v_196 ?v_195))) ?v_154))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_106 0) (or (and (and (and (= x_107 0) (< x_88 x_91)) (<= x_91 x_85)) (= x_102 x_91)) (and (and (and (= x_107 1) (< x_88 x_85)) (<= x_85 x_91)) (= x_102 x_85)))) ?v_197) ?v_219) ?v_198) ?v_220) ?v_203) ?v_204) ?v_205) ?v_206) ?v_207) (and (and (and (and (and (and (and (and (and (= x_106 1) (or (or (and (and (and (and (and (= x_108 0) ?v_199) ?v_215) ?v_201) ?v_197) ?v_198) (and (and (and (and (and (= x_108 1) ?v_199) ?v_214) ?v_200) ?v_202) ?v_197)) (and (and (and (and (= x_108 2) (not ?v_199)) (ite (or ?v_217 ?v_216) (or ?v_200 ?v_201) (= x_98 x_87))) (= x_104 (+ x_90 1))) (= x_103 (ite ?v_201 1 0))))) ?v_222) (ite ?v_161 (and (<= (+ x_88 ?v_6) x_105) (<= x_105 (+ (+ x_88 x_51) 1))) (ite ?v_202 (and (<= (+ x_88 ?v_46) x_105) (<= x_105 (+ x_88 ?v_47))) (and (<= (+ x_88 ?v_48) x_105) (<= x_105 (+ x_88 ?v_49)))))) ?v_218) ?v_203) ?v_204) ?v_205) ?v_206) ?v_207)) (and (and (and (and (and (and (and (and (= x_106 2) (or (and (and (and (and (= x_109 0) ?v_208) ?v_209) (= x_99 (+ x_88 x_53))) x_20) (and (and (and (and (= x_109 1) ?v_208) x_18) (= x_99 (+ x_88 ?v_56))) ?v_171))) (or (and (and (and (= x_110 0) ?v_211) (or (= x_100 0) ?v_213)) ?v_210) (and (and (= x_110 1) (not ?v_211)) ?v_205))) (or (or (or (and (and (and (and (= x_111 0) ?v_209) ?v_212) ?v_174) ?v_207) (and (and (and (and (= x_111 1) ?v_209) ?v_212) ?v_179) (= x_21 0))) (and (and (and (and (= x_111 2) ?v_209) (< x_19 9)) (= x_101 (ite (or ?v_213 (= x_19 8)) (ite ?v_214 3 x_87) (ite ?v_215 2 x_87)))) (= x_21 (+ x_19 1)))) (and (and (and (= x_111 3) x_18) (= x_101 (ite ?v_216 1 (ite ?v_217 0 x_87)))) ?v_206))) ?v_218) ?v_197) ?v_219) ?v_198) ?v_220))) (or (or (or (or (and (and ?v_223 (or (or ?v_231 ?v_232) ?v_234)) ?v_185) (and (and ?v_223 (or (and ?v_224 (not ?v_225)) (and ?v_226 ?v_227))) ?v_192)) (and (and (and (and (and ?v_223 ?v_221) ?v_222) ?v_228) ?v_225) ?v_229)) (and ?v_230 ?v_192)) (and (and ?v_267 (or (or (and ?v_231 ?v_233) (and ?v_232 ?v_233)) (and ?v_234 ?v_233))) ?v_192))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_92 0) (or (and (and (and (= x_93 0) (< x_74 x_77)) (<= x_77 x_71)) (= x_88 x_77)) (and (and (and (= x_93 1) (< x_74 x_71)) (<= x_71 x_77)) (= x_88 x_71)))) ?v_235) ?v_257) ?v_236) ?v_258) ?v_241) ?v_242) ?v_243) ?v_244) ?v_245) (and (and (and (and (and (and (and (and (and (= x_92 1) (or (or (and (and (and (and (and (= x_94 0) ?v_237) ?v_253) ?v_239) ?v_235) ?v_236) (and (and (and (and (and (= x_94 1) ?v_237) ?v_252) ?v_238) ?v_240) ?v_235)) (and (and (and (and (= x_94 2) (not ?v_237)) (ite (or ?v_255 ?v_254) (or ?v_238 ?v_239) (= x_84 x_73))) (= x_90 (+ x_76 1))) (= x_89 (ite ?v_239 1 0))))) ?v_260) (ite ?v_199 (and (<= (+ x_74 ?v_6) x_91) (<= x_91 (+ (+ x_74 x_51) 1))) (ite ?v_240 (and (<= (+ x_74 ?v_46) x_91) (<= x_91 (+ x_74 ?v_47))) (and (<= (+ x_74 ?v_48) x_91) (<= x_91 (+ x_74 ?v_49)))))) ?v_256) ?v_241) ?v_242) ?v_243) ?v_244) ?v_245)) (and (and (and (and (and (and (and (and (= x_92 2) (or (and (and (and (and (= x_95 0) ?v_246) ?v_247) (= x_85 (+ x_74 x_53))) x_18) (and (and (and (and (= x_95 1) ?v_246) x_16) (= x_85 (+ x_74 ?v_56))) ?v_209))) (or (and (and (and (= x_96 0) ?v_249) (or (= x_86 0) ?v_251)) ?v_248) (and (and (= x_96 1) (not ?v_249)) ?v_243))) (or (or (or (and (and (and (and (= x_97 0) ?v_247) ?v_250) ?v_212) ?v_245) (and (and (and (and (= x_97 1) ?v_247) ?v_250) ?v_217) (= x_19 0))) (and (and (and (and (= x_97 2) ?v_247) (< x_17 9)) (= x_87 (ite (or ?v_251 (= x_17 8)) (ite ?v_252 3 x_73) (ite ?v_253 2 x_73)))) (= x_19 (+ x_17 1)))) (and (and (and (= x_97 3) x_16) (= x_87 (ite ?v_254 1 (ite ?v_255 0 x_73)))) ?v_244))) ?v_256) ?v_235) ?v_257) ?v_236) ?v_258))) (or (or (or (or (and (and ?v_261 (or (or ?v_269 ?v_270) ?v_272)) ?v_223) (and (and ?v_261 (or (and ?v_262 (not ?v_263)) (and ?v_264 ?v_265))) ?v_230)) (and (and (and (and (and ?v_261 ?v_259) ?v_260) ?v_266) ?v_263) ?v_267)) (and ?v_268 ?v_230)) (and (and ?v_305 (or (or (and ?v_269 ?v_271) (and ?v_270 ?v_271)) (and ?v_272 ?v_271))) ?v_230))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_78 0) (or (and (and (and (= x_79 0) (< x_60 x_63)) (<= x_63 x_57)) (= x_74 x_63)) (and (and (and (= x_79 1) (< x_60 x_57)) (<= x_57 x_63)) (= x_74 x_57)))) ?v_273) ?v_295) ?v_274) ?v_296) ?v_279) ?v_280) ?v_281) ?v_282) ?v_283) (and (and (and (and (and (and (and (and (and (= x_78 1) (or (or (and (and (and (and (and (= x_80 0) ?v_275) ?v_291) ?v_277) ?v_273) ?v_274) (and (and (and (and (and (= x_80 1) ?v_275) ?v_290) ?v_276) ?v_278) ?v_273)) (and (and (and (and (= x_80 2) (not ?v_275)) (ite (or ?v_293 ?v_292) (or ?v_276 ?v_277) (= x_70 x_59))) (= x_76 (+ x_62 1))) (= x_75 (ite ?v_277 1 0))))) ?v_298) (ite ?v_237 (and (<= (+ x_60 ?v_6) x_77) (<= x_77 (+ (+ x_60 x_51) 1))) (ite ?v_278 (and (<= (+ x_60 ?v_46) x_77) (<= x_77 (+ x_60 ?v_47))) (and (<= (+ x_60 ?v_48) x_77) (<= x_77 (+ x_60 ?v_49)))))) ?v_294) ?v_279) ?v_280) ?v_281) ?v_282) ?v_283)) (and (and (and (and (and (and (and (and (= x_78 2) (or (and (and (and (and (= x_81 0) ?v_284) ?v_285) (= x_71 (+ x_60 x_53))) x_16) (and (and (and (and (= x_81 1) ?v_284) x_14) (= x_71 (+ x_60 ?v_56))) ?v_247))) (or (and (and (and (= x_82 0) ?v_287) (or (= x_72 0) ?v_289)) ?v_286) (and (and (= x_82 1) (not ?v_287)) ?v_281))) (or (or (or (and (and (and (and (= x_83 0) ?v_285) ?v_288) ?v_250) ?v_283) (and (and (and (and (= x_83 1) ?v_285) ?v_288) ?v_255) (= x_17 0))) (and (and (and (and (= x_83 2) ?v_285) (< x_15 9)) (= x_73 (ite (or ?v_289 (= x_15 8)) (ite ?v_290 3 x_59) (ite ?v_291 2 x_59)))) (= x_17 (+ x_15 1)))) (and (and (and (= x_83 3) x_14) (= x_73 (ite ?v_292 1 (ite ?v_293 0 x_59)))) ?v_282))) ?v_294) ?v_273) ?v_295) ?v_274) ?v_296))) (or (or (or (or (and (and ?v_299 (or (or ?v_307 ?v_308) ?v_310)) ?v_261) (and (and ?v_299 (or (and ?v_300 (not ?v_301)) (and ?v_302 ?v_303))) ?v_268)) (and (and (and (and (and ?v_299 ?v_297) ?v_298) ?v_304) ?v_301) ?v_305)) (and ?v_306 ?v_268)) (and (and ?v_343 (or (or (and ?v_307 ?v_309) (and ?v_308 ?v_309)) (and ?v_310 ?v_309))) ?v_268))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_64 0) (or (and (and (and (= x_65 0) (< x_41 x_46)) (<= x_46 x_34)) (= x_60 x_46)) (and (and (and (= x_65 1) (< x_41 x_34)) (<= x_34 x_46)) (= x_60 x_34)))) ?v_311) ?v_333) ?v_312) ?v_334) ?v_317) ?v_318) ?v_319) ?v_320) ?v_321) (and (and (and (and (and (and (and (and (and (= x_64 1) (or (or (and (and (and (and (and (= x_66 0) ?v_313) ?v_329) ?v_315) ?v_311) ?v_312) (and (and (and (and (and (= x_66 1) ?v_313) ?v_328) ?v_314) ?v_316) ?v_311)) (and (and (and (and (= x_66 2) (not ?v_313)) (ite (or ?v_331 ?v_330) (or ?v_314 ?v_315) (= x_56 x_39))) (= x_62 (+ x_45 1))) (= x_61 (ite ?v_315 1 0))))) ?v_336) (ite ?v_275 (and (<= (+ x_41 ?v_6) x_63) (<= x_63 (+ (+ x_41 x_51) 1))) (ite ?v_316 (and (<= (+ x_41 ?v_46) x_63) (<= x_63 (+ x_41 ?v_47))) (and (<= (+ x_41 ?v_48) x_63) (<= x_63 (+ x_41 ?v_49)))))) ?v_332) ?v_317) ?v_318) ?v_319) ?v_320) ?v_321)) (and (and (and (and (and (and (and (and (= x_64 2) (or (and (and (and (and (= x_67 0) ?v_322) ?v_323) (= x_57 (+ x_41 x_53))) x_14) (and (and (and (and (= x_67 1) ?v_322) x_12) (= x_57 (+ x_41 ?v_56))) ?v_285))) (or (and (and (and (= x_68 0) ?v_325) (or (= x_58 0) ?v_327)) ?v_324) (and (and (= x_68 1) (not ?v_325)) ?v_319))) (or (or (or (and (and (and (and (= x_69 0) ?v_323) ?v_326) ?v_288) ?v_321) (and (and (and (and (= x_69 1) ?v_323) ?v_326) ?v_293) (= x_15 0))) (and (and (and (and (= x_69 2) ?v_323) (< x_13 9)) (= x_59 (ite (or ?v_327 (= x_13 8)) (ite ?v_328 3 x_39) (ite ?v_329 2 x_39)))) (= x_15 (+ x_13 1)))) (and (and (and (= x_69 3) x_12) (= x_59 (ite ?v_330 1 (ite ?v_331 0 x_39)))) ?v_320))) ?v_332) ?v_311) ?v_333) ?v_312) ?v_334))) (or (or (or (or (and (and ?v_337 (or (or ?v_345 ?v_346) ?v_348)) ?v_299) (and (and ?v_337 (or (and ?v_338 (not ?v_339)) (and ?v_340 ?v_341))) ?v_306)) (and (and (and (and (and ?v_337 ?v_335) ?v_336) ?v_342) ?v_339) ?v_343)) (and ?v_344 ?v_306)) (and (and ?v_381 (or (or (and ?v_345 ?v_347) (and ?v_346 ?v_347)) (and ?v_348 ?v_347))) ?v_306))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_48 0) (or (and (and (and (= x_49 0) (< x_36 x_47)) (<= x_47 x_35)) (= x_41 x_47)) (and (and (and (= x_49 1) (< x_36 x_35)) (<= x_35 x_47)) (= x_41 x_35)))) ?v_349) ?v_371) ?v_350) ?v_372) ?v_355) ?v_356) ?v_357) ?v_358) ?v_359) (and (and (and (and (and (and (and (and (and (= x_48 1) (or (or (and (and (and (and (and (= x_50 0) ?v_351) ?v_367) ?v_353) ?v_349) ?v_350) (and (and (and (and (and (= x_50 1) ?v_351) ?v_366) ?v_352) ?v_354) ?v_349)) (and (and (and (and (= x_50 2) (not ?v_351)) (ite (or ?v_369 ?v_368) (or ?v_352 ?v_353) (= x_33 x_40))) (= x_45 (+ x_32 1))) (= x_42 (ite ?v_353 1 0))))) ?v_374) (ite ?v_313 (and (<= (+ x_36 ?v_6) x_46) (<= x_46 (+ (+ x_36 x_51) 1))) (ite ?v_354 (and (<= (+ x_36 ?v_46) x_46) (<= x_46 (+ x_36 ?v_47))) (and (<= (+ x_36 ?v_48) x_46) (<= x_46 (+ x_36 ?v_49)))))) ?v_370) ?v_355) ?v_356) ?v_357) ?v_358) ?v_359)) (and (and (and (and (and (and (and (and (= x_48 2) (or (and (and (and (and (= x_52 0) ?v_360) ?v_361) (= x_34 (+ x_36 x_53))) x_12) (and (and (and (and (= x_52 1) ?v_360) x_10) (= x_34 (+ x_36 ?v_56))) ?v_323))) (or (and (and (and (= x_54 0) ?v_363) (or (= x_37 0) ?v_365)) ?v_362) (and (and (= x_54 1) (not ?v_363)) ?v_357))) (or (or (or (and (and (and (and (= x_55 0) ?v_361) ?v_364) ?v_326) ?v_359) (and (and (and (and (= x_55 1) ?v_361) ?v_364) ?v_331) (= x_13 0))) (and (and (and (and (= x_55 2) ?v_361) (< x_11 9)) (= x_39 (ite (or ?v_365 (= x_11 8)) (ite ?v_366 3 x_40) (ite ?v_367 2 x_40)))) (= x_13 (+ x_11 1)))) (and (and (and (= x_55 3) x_10) (= x_39 (ite ?v_368 1 (ite ?v_369 0 x_40)))) ?v_358))) ?v_370) ?v_349) ?v_371) ?v_350) ?v_372))) (or (or (or (or (and (and ?v_375 (or (or ?v_383 ?v_384) ?v_386)) ?v_337) (and (and ?v_375 (or (and ?v_376 (not ?v_377)) (and ?v_378 ?v_379))) ?v_344)) (and (and (and (and (and ?v_375 ?v_373) ?v_374) ?v_380) ?v_377) ?v_381)) (and ?v_382 ?v_344)) (and (and (= x_0 0) (or (or (and ?v_383 ?v_385) (and ?v_384 ?v_385)) (and ?v_386 ?v_385))) ?v_344))) ?v_35)))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/tests/unsat/reg_lra_fm1.smt2 b/tests/unsat/reg_lra_fm1.smt2
new file mode 100644
index 00000000..bee80771
--- /dev/null
+++ b/tests/unsat/reg_lra_fm1.smt2
@@ -0,0 +1,36 @@
+
+; expect: unsat
+; intermediate problem in tests/unsat/clocksynchro_2clocks.worst_case_skew.base.smt2
+
+(set-logic QF_LRA)
+(declare-fun x_0 () Real)
+(declare-fun x_1 () Real)
+(declare-fun x_2 () Real)
+(declare-fun x_3 () Real)
+(declare-fun x_4 () Real)
+(declare-fun x_5 () Real)
+(declare-fun x_6 () Real)
+(declare-fun x_7 () Real)
+
+(assert (< (+ (/ 2335 666) x_5 x_6 (* (/ 2 999) x_7) (* (/ 2 999) x_4)) 0))
+(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_2) 0))
+(assert (<= (+ (/ 999 1000) x_0 (* -1 x_2)) 0))
+(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_1) 0))
+(assert (<= (+ (/ 999 1000) x_0 (- 0 x_1)) 0))
+(assert (= x_0 0))
+(assert
+  (<= (+
+    (/ 1502501 999000)
+    (* (/ 1001 999) x_5)
+    (* (/ 1001 999) x_6)
+    (* -1 x_7)
+    (* (/ 1001 999) x_3))
+    0))
+
+(assert (< (+ (/ 1001 2) (* (/ 999 2) x_6) x_7 (* (/ -999 2) x_4)) 0))
+(assert (<= (+ (/ 1001 999) x_5 (* -1 x_6) (* (/ 1001 1998) x_4)) 0))
+(assert (< (* -1 x_5) 0))
+(assert (< (* -1 x_4) 0))
+(assert (< (* -1 x_3) 0))
+
+(check-sat)
diff --git a/tests/unsat/sc-6.base.cvc.smt2 b/tests/unsat/sc-6.base.cvc.smt2
new file mode 100644
index 00000000..3d0f10c6
--- /dev/null
+++ b/tests/unsat/sc-6.base.cvc.smt2
@@ -0,0 +1,144 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_LRA)
+(set-info :source |
+Fully parameterized specification and verification of a synchronizer   
+circuit modeling metastability at various levels of refinement.     
+A paper describing this specification, to be published in Designing     
+Correct Circuits (DCC), 2006, is available from the authors.            
+
+Geoffrey Brown, Indiana University <geobrown@cs.indiana.edu>
+Lee Pike, Galois Connections, Inc. <leepike@galois.com>
+
+Translated into CVC format by Leonardo de Moura.
+
+This benchmark was automatically translated into SMT-LIB format from
+CVC format using CVC Lite
+
+|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun x_0 () Bool)
+(declare-fun x_1 () Bool)
+(declare-fun x_2 () Real)
+(declare-fun x_3 () Bool)
+(declare-fun x_4 () Bool)
+(declare-fun x_5 () Bool)
+(declare-fun x_6 () Real)
+(declare-fun x_7 () Bool)
+(declare-fun x_8 () Real)
+(declare-fun x_9 () Real)
+(declare-fun x_10 () Real)
+(declare-fun x_11 () Real)
+(declare-fun x_12 () Real)
+(declare-fun x_13 () Bool)
+(declare-fun x_14 () Real)
+(declare-fun x_15 () Real)
+(declare-fun x_16 () Real)
+(declare-fun x_17 () Real)
+(declare-fun x_18 () Real)
+(declare-fun x_19 () Real)
+(declare-fun x_20 () Bool)
+(declare-fun x_21 () Bool)
+(declare-fun x_22 () Bool)
+(declare-fun x_23 () Bool)
+(declare-fun x_24 () Real)
+(declare-fun x_25 () Bool)
+(declare-fun x_26 () Real)
+(declare-fun x_27 () Real)
+(declare-fun x_28 () Real)
+(declare-fun x_29 () Real)
+(declare-fun x_30 () Real)
+(declare-fun x_31 () Real)
+(declare-fun x_32 () Real)
+(declare-fun x_33 () Real)
+(declare-fun x_34 () Real)
+(declare-fun x_35 () Real)
+(declare-fun x_36 () Real)
+(declare-fun x_37 () Bool)
+(declare-fun x_38 () Real)
+(declare-fun x_39 () Real)
+(declare-fun x_40 () Bool)
+(declare-fun x_41 () Bool)
+(declare-fun x_42 () Bool)
+(declare-fun x_43 () Bool)
+(declare-fun x_44 () Real)
+(declare-fun x_45 () Bool)
+(declare-fun x_46 () Real)
+(declare-fun x_47 () Real)
+(declare-fun x_48 () Real)
+(declare-fun x_49 () Real)
+(declare-fun x_50 () Real)
+(declare-fun x_51 () Real)
+(declare-fun x_52 () Real)
+(declare-fun x_53 () Real)
+(declare-fun x_54 () Real)
+(declare-fun x_55 () Bool)
+(declare-fun x_56 () Real)
+(declare-fun x_57 () Real)
+(declare-fun x_58 () Bool)
+(declare-fun x_59 () Bool)
+(declare-fun x_60 () Bool)
+(declare-fun x_61 () Bool)
+(declare-fun x_62 () Real)
+(declare-fun x_63 () Bool)
+(declare-fun x_64 () Real)
+(declare-fun x_65 () Real)
+(declare-fun x_66 () Real)
+(declare-fun x_67 () Real)
+(declare-fun x_68 () Real)
+(declare-fun x_69 () Real)
+(declare-fun x_70 () Real)
+(declare-fun x_71 () Real)
+(declare-fun x_72 () Real)
+(declare-fun x_73 () Bool)
+(declare-fun x_74 () Real)
+(declare-fun x_75 () Real)
+(declare-fun x_76 () Bool)
+(declare-fun x_77 () Bool)
+(declare-fun x_78 () Bool)
+(declare-fun x_79 () Bool)
+(declare-fun x_80 () Real)
+(declare-fun x_81 () Bool)
+(declare-fun x_82 () Real)
+(declare-fun x_83 () Real)
+(declare-fun x_84 () Real)
+(declare-fun x_85 () Real)
+(declare-fun x_86 () Real)
+(declare-fun x_87 () Real)
+(declare-fun x_88 () Real)
+(declare-fun x_89 () Real)
+(declare-fun x_90 () Real)
+(declare-fun x_91 () Bool)
+(declare-fun x_92 () Real)
+(declare-fun x_93 () Real)
+(declare-fun x_94 () Bool)
+(declare-fun x_95 () Bool)
+(declare-fun x_96 () Bool)
+(declare-fun x_97 () Bool)
+(declare-fun x_98 () Real)
+(declare-fun x_99 () Bool)
+(declare-fun x_100 () Real)
+(declare-fun x_101 () Real)
+(declare-fun x_102 () Real)
+(declare-fun x_103 () Real)
+(declare-fun x_104 () Real)
+(declare-fun x_105 () Real)
+(declare-fun x_106 () Real)
+(declare-fun x_107 () Real)
+(declare-fun x_108 () Real)
+(declare-fun x_109 () Bool)
+(declare-fun x_110 () Real)
+(declare-fun x_111 () Real)
+(declare-fun x_112 () Bool)
+(declare-fun x_113 () Bool)
+(declare-fun x_114 () Bool)
+(declare-fun x_115 () Bool)
+(declare-fun x_116 () Real)
+(declare-fun x_117 () Bool)
+(declare-fun x_118 () Real)
+(declare-fun x_119 () Real)
+(declare-fun x_120 () Real)
+(declare-fun x_121 () Real)
+(assert (let ((?v_73 (= x_6 x_9)) (?v_70 (= x_2 x_11))) (let ((?v_75 (not ?v_70)) (?v_66 (= x_13 x_7)) (?v_67 (= x_14 x_15)) (?v_71 (ite (<= x_6 x_2) x_6 x_2)) (?v_65 (ite (<= x_2 x_6) x_2 x_6)) (?v_58 (= x_32 x_8)) (?v_59 (= x_9 x_33)) (?v_60 (= x_34 x_10)) (?v_56 (= x_11 x_35))) (let ((?v_61 (not ?v_56)) (?v_64 (= x_36 x_12)) (?v_53 (= x_37 x_13)) (?v_54 (= x_38 x_14)) (?v_57 (ite (<= x_9 x_11) x_9 x_11)) (?v_52 (ite (<= x_11 x_9) x_11 x_9)) (?v_45 (= x_50 x_32)) (?v_46 (= x_33 x_51)) (?v_47 (= x_52 x_34)) (?v_43 (= x_35 x_53))) (let ((?v_48 (not ?v_43)) (?v_51 (= x_54 x_36)) (?v_40 (= x_55 x_37)) (?v_41 (= x_56 x_38)) (?v_44 (ite (<= x_33 x_35) x_33 x_35)) (?v_39 (ite (<= x_35 x_33) x_35 x_33)) (?v_32 (= x_68 x_50)) (?v_33 (= x_51 x_69)) (?v_34 (= x_70 x_52)) (?v_30 (= x_53 x_71))) (let ((?v_35 (not ?v_30)) (?v_38 (= x_72 x_54)) (?v_27 (= x_73 x_55)) (?v_28 (= x_74 x_56)) (?v_31 (ite (<= x_51 x_53) x_51 x_53)) (?v_26 (ite (<= x_53 x_51) x_53 x_51)) (?v_19 (= x_86 x_68)) (?v_20 (= x_69 x_87)) (?v_21 (= x_88 x_70)) (?v_17 (= x_71 x_89))) (let ((?v_22 (not ?v_17)) (?v_25 (= x_90 x_72)) (?v_14 (= x_91 x_73)) (?v_15 (= x_92 x_74)) (?v_18 (ite (<= x_69 x_71) x_69 x_71)) (?v_13 (ite (<= x_71 x_69) x_71 x_69)) (?v_6 (= x_104 x_86)) (?v_7 (= x_87 x_105)) (?v_8 (= x_106 x_88)) (?v_4 (= x_89 x_107))) (let ((?v_9 (not ?v_4)) (?v_12 (= x_108 x_90)) (?v_1 (= x_109 x_91)) (?v_2 (= x_110 x_92)) (?v_5 (ite (<= x_87 x_89) x_87 x_89)) (?v_0 (ite (<= x_89 x_87) x_89 x_87)) (?v_68 (not x_7)) (?v_3 (= x_113 x_95)) (?v_11 (= x_92 x_110)) (?v_16 (= x_95 x_77)) (?v_24 (= x_74 x_92)) (?v_29 (= x_77 x_59)) (?v_37 (= x_56 x_74)) (?v_42 (= x_59 x_41)) (?v_50 (= x_38 x_56)) (?v_55 (= x_41 x_21)) (?v_63 (= x_14 x_38)) (?v_69 (= x_21 x_3)) (?v_78 (= x_15 x_14)) (?v_76 (not (>= ?v_71 0))) (?v_72 (= x_8 0)) (?v_74 (= x_10 0)) (?v_79 (= x_12 0))) (let ((?v_10 (+ ?v_5 x_18)) (?v_23 (+ ?v_18 x_18)) (?v_36 (+ ?v_31 x_18)) (?v_49 (+ ?v_44 x_18)) (?v_62 (+ ?v_57 x_18)) (?v_77 (+ ?v_71 x_18))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (> x_16 0) (> x_17 0)) (>= x_18 0)) (< x_18 x_16)) (< x_18 x_17)) (>= x_30 0)) (< x_30 x_16)) (< x_30 x_17)) (not x_0)) (not x_1)) (>= x_2 0)) (not x_3)) (not x_4)) (not x_5)) (>= x_6 0)) ?v_68) (or (and (and (and (and (and (and (and (and (and (= x_111 0) (= x_112 x_99)) (= ?v_0 x_89)) (<= (+ ?v_0 x_16) x_107)) (or ?v_3 (= x_113 x_94))) (= x_114 x_96)) (= x_115 x_97)) (= x_105 x_87)) ?v_1) ?v_2) (and (and (and (and (and (and (and (and (and (= x_111 1) (= x_115 x_96)) (= ?v_0 x_87)) (<= (+ ?v_0 x_17) x_105)) (or (and (and (= x_116 0) ?v_1) ?v_2) (and (and (= x_116 1) (= x_91 x_97)) (= x_109 (not x_91))))) (= x_117 x_99)) (= x_112 x_94)) (= x_118 x_100)) (= x_107 x_89)) ?v_3))) (or (or (and (and (and (= x_119 0) ?v_9) (or (not (<= x_86 ?v_5)) (= x_117 x_91))) ?v_6) (and (and (and (= x_119 1) ?v_4) (xor x_91 x_109)) (= x_104 ?v_10))) (and (and (and (= x_119 2) ?v_4) (= x_91 x_109)) ?v_6))) (or (or (and (and (and (= x_120 0) (not ?v_7)) (or (not (<= x_88 ?v_0)) (= x_114 x_95))) ?v_8) (and (and (and (= x_120 1) ?v_7) (xor x_95 x_113)) (= x_106 (+ ?v_0 x_30)))) (and (and (and (= x_120 2) ?v_7) (= x_95 x_113)) ?v_8))) (or (or (and (and (and (= x_121 0) ?v_9) (or (not (<= x_90 ?v_5)) (= x_118 x_92))) ?v_12) (and (and (and (= x_121 1) ?v_4) (not ?v_11)) (= x_108 ?v_10))) (and (and (and (= x_121 2) ?v_4) ?v_11) ?v_12))) (or (and (and (and (and (and (and (and (and (and (= x_93 0) (= x_94 x_81)) (= ?v_13 x_71)) (<= (+ ?v_13 x_16) x_89)) (or ?v_16 (= x_95 x_76))) (= x_96 x_78)) (= x_97 x_79)) (= x_87 x_69)) ?v_14) ?v_15) (and (and (and (and (and (and (and (and (and (= x_93 1) (= x_97 x_78)) (= ?v_13 x_69)) (<= (+ ?v_13 x_17) x_87)) (or (and (and (= x_98 0) ?v_14) ?v_15) (and (and (= x_98 1) (= x_73 x_79)) (= x_91 (not x_73))))) (= x_99 x_81)) (= x_94 x_76)) (= x_100 x_82)) (= x_89 x_71)) ?v_16))) (or (or (and (and (and (= x_101 0) ?v_22) (or (not (<= x_68 ?v_18)) (= x_99 x_73))) ?v_19) (and (and (and (= x_101 1) ?v_17) (xor x_73 x_91)) (= x_86 ?v_23))) (and (and (and (= x_101 2) ?v_17) (= x_73 x_91)) ?v_19))) (or (or (and (and (and (= x_102 0) (not ?v_20)) (or (not (<= x_70 ?v_13)) (= x_96 x_77))) ?v_21) (and (and (and (= x_102 1) ?v_20) (xor x_77 x_95)) (= x_88 (+ ?v_13 x_30)))) (and (and (and (= x_102 2) ?v_20) (= x_77 x_95)) ?v_21))) (or (or (and (and (and (= x_103 0) ?v_22) (or (not (<= x_72 ?v_18)) (= x_100 x_74))) ?v_25) (and (and (and (= x_103 1) ?v_17) (not ?v_24)) (= x_90 ?v_23))) (and (and (and (= x_103 2) ?v_17) ?v_24) ?v_25))) (or (and (and (and (and (and (and (and (and (and (= x_75 0) (= x_76 x_63)) (= ?v_26 x_53)) (<= (+ ?v_26 x_16) x_71)) (or ?v_29 (= x_77 x_58))) (= x_78 x_60)) (= x_79 x_61)) (= x_69 x_51)) ?v_27) ?v_28) (and (and (and (and (and (and (and (and (and (= x_75 1) (= x_79 x_60)) (= ?v_26 x_51)) (<= (+ ?v_26 x_17) x_69)) (or (and (and (= x_80 0) ?v_27) ?v_28) (and (and (= x_80 1) (= x_55 x_61)) (= x_73 (not x_55))))) (= x_81 x_63)) (= x_76 x_58)) (= x_82 x_64)) (= x_71 x_53)) ?v_29))) (or (or (and (and (and (= x_83 0) ?v_35) (or (not (<= x_50 ?v_31)) (= x_81 x_55))) ?v_32) (and (and (and (= x_83 1) ?v_30) (xor x_55 x_73)) (= x_68 ?v_36))) (and (and (and (= x_83 2) ?v_30) (= x_55 x_73)) ?v_32))) (or (or (and (and (and (= x_84 0) (not ?v_33)) (or (not (<= x_52 ?v_26)) (= x_78 x_59))) ?v_34) (and (and (and (= x_84 1) ?v_33) (xor x_59 x_77)) (= x_70 (+ ?v_26 x_30)))) (and (and (and (= x_84 2) ?v_33) (= x_59 x_77)) ?v_34))) (or (or (and (and (and (= x_85 0) ?v_35) (or (not (<= x_54 ?v_31)) (= x_82 x_56))) ?v_38) (and (and (and (= x_85 1) ?v_30) (not ?v_37)) (= x_72 ?v_36))) (and (and (and (= x_85 2) ?v_30) ?v_37) ?v_38))) (or (and (and (and (and (and (and (and (and (and (= x_57 0) (= x_58 x_45)) (= ?v_39 x_35)) (<= (+ ?v_39 x_16) x_53)) (or ?v_42 (= x_59 x_40))) (= x_60 x_42)) (= x_61 x_43)) (= x_51 x_33)) ?v_40) ?v_41) (and (and (and (and (and (and (and (and (and (= x_57 1) (= x_61 x_42)) (= ?v_39 x_33)) (<= (+ ?v_39 x_17) x_51)) (or (and (and (= x_62 0) ?v_40) ?v_41) (and (and (= x_62 1) (= x_37 x_43)) (= x_55 (not x_37))))) (= x_63 x_45)) (= x_58 x_40)) (= x_64 x_46)) (= x_53 x_35)) ?v_42))) (or (or (and (and (and (= x_65 0) ?v_48) (or (not (<= x_32 ?v_44)) (= x_63 x_37))) ?v_45) (and (and (and (= x_65 1) ?v_43) (xor x_37 x_55)) (= x_50 ?v_49))) (and (and (and (= x_65 2) ?v_43) (= x_37 x_55)) ?v_45))) (or (or (and (and (and (= x_66 0) (not ?v_46)) (or (not (<= x_34 ?v_39)) (= x_60 x_41))) ?v_47) (and (and (and (= x_66 1) ?v_46) (xor x_41 x_59)) (= x_52 (+ ?v_39 x_30)))) (and (and (and (= x_66 2) ?v_46) (= x_41 x_59)) ?v_47))) (or (or (and (and (and (= x_67 0) ?v_48) (or (not (<= x_36 ?v_44)) (= x_64 x_38))) ?v_51) (and (and (and (= x_67 1) ?v_43) (not ?v_50)) (= x_54 ?v_49))) (and (and (and (= x_67 2) ?v_43) ?v_50) ?v_51))) (or (and (and (and (and (and (and (and (and (and (= x_39 0) (= x_40 x_25)) (= ?v_52 x_11)) (<= (+ ?v_52 x_16) x_35)) (or ?v_55 (= x_41 x_20))) (= x_42 x_22)) (= x_43 x_23)) (= x_33 x_9)) ?v_53) ?v_54) (and (and (and (and (and (and (and (and (and (= x_39 1) (= x_43 x_22)) (= ?v_52 x_9)) (<= (+ ?v_52 x_17) x_33)) (or (and (and (= x_44 0) ?v_53) ?v_54) (and (and (= x_44 1) (= x_13 x_23)) (= x_37 (not x_13))))) (= x_45 x_25)) (= x_40 x_20)) (= x_46 x_26)) (= x_35 x_11)) ?v_55))) (or (or (and (and (and (= x_47 0) ?v_61) (or (not (<= x_8 ?v_57)) (= x_45 x_13))) ?v_58) (and (and (and (= x_47 1) ?v_56) (xor x_13 x_37)) (= x_32 ?v_62))) (and (and (and (= x_47 2) ?v_56) (= x_13 x_37)) ?v_58))) (or (or (and (and (and (= x_48 0) (not ?v_59)) (or (not (<= x_10 ?v_52)) (= x_42 x_21))) ?v_60) (and (and (and (= x_48 1) ?v_59) (xor x_21 x_41)) (= x_34 (+ ?v_52 x_30)))) (and (and (and (= x_48 2) ?v_59) (= x_21 x_41)) ?v_60))) (or (or (and (and (and (= x_49 0) ?v_61) (or (not (<= x_12 ?v_57)) (= x_46 x_14))) ?v_64) (and (and (and (= x_49 1) ?v_56) (not ?v_63)) (= x_36 ?v_62))) (and (and (and (= x_49 2) ?v_56) ?v_63) ?v_64))) (or (and (and (and (and (and (and (and (and (and (= x_19 0) (= x_20 x_0)) (= ?v_65 x_2)) (<= (+ ?v_65 x_16) x_11)) (or ?v_69 (= x_21 x_1))) (= x_22 x_4)) (= x_23 x_5)) (= x_9 x_6)) ?v_66) ?v_67) (and (and (and (and (and (and (and (and (and (= x_19 1) (= x_23 x_4)) (= ?v_65 x_6)) (<= (+ ?v_65 x_17) x_9)) (or (and (and (= x_24 0) ?v_66) ?v_67) (and (and (= x_24 1) (= x_7 x_5)) (= x_13 ?v_68)))) (= x_25 x_0)) (= x_20 x_1)) (= x_26 x_27)) (= x_11 x_2)) ?v_69))) (or (or (and (and (and (= x_28 0) ?v_75) (or ?v_76 (= x_25 x_7))) ?v_72) (and (and (and (= x_28 1) ?v_70) (xor x_7 x_13)) (= x_8 ?v_77))) (and (and (and (= x_28 2) ?v_70) (= x_7 x_13)) ?v_72))) (or (or (and (and (and (= x_29 0) (not ?v_73)) (or (not (>= ?v_65 0)) (= x_22 x_3))) ?v_74) (and (and (and (= x_29 1) ?v_73) (xor x_3 x_21)) (= x_10 (+ ?v_65 x_30)))) (and (and (and (= x_29 2) ?v_73) (= x_3 x_21)) ?v_74))) (or (or (and (and (and (= x_31 0) ?v_75) (or ?v_76 (= x_26 x_15))) ?v_79) (and (and (and (= x_31 1) ?v_70) (not ?v_78)) (= x_12 ?v_77))) (and (and (and (= x_31 2) ?v_70) ?v_78) ?v_79))) (or (or (or (or (or (or (and (xor x_112 x_113) (not (= x_118 x_110))) (and (xor x_94 x_95) (not (= x_100 x_92)))) (and (xor x_76 x_77) (not (= x_82 x_74)))) (and (xor x_58 x_59) (not (= x_64 x_56)))) (and (xor x_40 x_41) (not (= x_46 x_38)))) (and (xor x_20 x_21) (not (= x_26 x_14)))) (and (xor x_1 x_3) (not (= x_27 x_15))))))))))))))
+(check-sat)
+(exit)
diff --git a/tests/unsat/smtlib.624916.smt2 b/tests/unsat/smtlib.624916.smt2
new file mode 100644
index 00000000..e22880db
--- /dev/null
+++ b/tests/unsat/smtlib.624916.smt2
@@ -0,0 +1,16 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UFLRA)
+(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011.  Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-sort S1 0)
+(declare-fun f1 () S1)
+(declare-fun f2 () S1)
+(declare-fun f3 (Real) Real)
+(declare-fun f4 () Real)
+(declare-fun f5 () Real)
+(assert (not (= f1 f2)))
+(assert (= (f3 f4) (- 1)))
+(assert (not (=> (= f5 f4) (not (= (f3 f5) 1.0)))))
+(check-sat)
+(exit)