diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml
index 5e720d2e..5f118c74 100644
--- a/src/base-term/Base_types.ml
+++ b/src/base-term/Base_types.ml
@@ -10,6 +10,7 @@ type lra_op = Sidekick_lra.op = Plus | Minus
 type 'a lra_view = 'a Sidekick_lra.lra_view =
   | LRA_pred of lra_pred * 'a * 'a
   | LRA_op of lra_op * 'a * 'a
+  | LRA_mult of Q.t * 'a
   | LRA_const of Q.t
   | LRA_other of 'a
 
@@ -234,6 +235,8 @@ let pp_term_view_gen ~pp_id ~pp_t out = function
         Fmt.fprintf out "(@[%s@ %a@ %a@])" (string_of_lra_pred p) pp_t a pp_t b
       | LRA_op (p, a, b) ->
         Fmt.fprintf out "(@[%s@ %a@ %a@])" (string_of_lra_op p) pp_t a pp_t b
+      | LRA_mult (n, x) ->
+        Fmt.fprintf out "(@[*@ %a@ %a@])" Q.pp_print n pp_t x
       | LRA_const q -> Q.pp_print out q
       | LRA_other x -> pp_t out x
     end
@@ -603,7 +606,9 @@ end = struct
             Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b)
           | LRA_op (p, a, b) ->
             Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b)
-          | LRA_const q -> Hash.combine2 83 (Hash.string @@ Q.to_string q)
+          | LRA_mult (n, x) ->
+            Hash.combine3 83 (Hash.string @@ Q.to_string n) (sub_hash x)
+          | LRA_const q -> Hash.combine2 84 (Hash.string @@ Q.to_string q)
           | LRA_other x -> sub_hash x
         end
 
@@ -623,8 +628,10 @@ end = struct
           | LRA_op(p1,a1,b1), LRA_op (p2,a2,b2) ->
             p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
           | LRA_const a1, LRA_const a2 -> Q.equal a1 a2
+          | LRA_mult (n1,x1), LRA_mult (n2,x2) -> Q.equal n1 n2 && sub_eq x1 x2
           | LRA_other x1, LRA_other x2 -> sub_eq x1 x2
-          | (LRA_pred _ | LRA_op _ | LRA_const _ | LRA_other _), _ -> false
+          | (LRA_pred _ | LRA_op _ | LRA_const _
+            | LRA_mult _ | LRA_other _), _ -> false
         end
       | (Bool _ | App_fun _ | Eq _ | Not _ | Ite _ | LRA _), _
         -> false
@@ -659,8 +666,8 @@ end = struct
     | Not u -> u.term_view
     | _ -> Not t
 
-  let ite a b c = Ite (a,b,c)
-  let lra l : t = LRA l
+  let[@inline] ite a b c = Ite (a,b,c)
+  let[@inline] lra l : t = LRA l
 
   let ty (t:t): Ty.t = match t with
     | Bool _ | Eq _ | Not _ -> Ty.bool
@@ -694,7 +701,7 @@ end = struct
     | LRA l ->
       begin match l with
         | LRA_pred _ -> Ty.bool
-        | LRA_op _ | LRA_const _ -> Ty.real
+        | LRA_op _ | LRA_const _ | LRA_mult _ -> Ty.real
         | LRA_other x -> x.term_ty
       end
 
@@ -708,8 +715,8 @@ end = struct
     | LRA l ->
       begin match l with
         | LRA_pred (_, a, b)|LRA_op (_, a, b) -> f a; f b
+        | LRA_mult (_,x) | LRA_other x -> f x
         | LRA_const _ -> ()
-        | LRA_other x -> f x
       end
 
   let map f view =
@@ -877,7 +884,9 @@ end = struct
   let app_cstor st c args : t = app_fun st (Fun.cstor c) args
 
   let[@inline] lra (st:state) (l:t lra_view) : t =
-    make st (Term_cell.lra l)
+    match l with
+    | LRA_other x -> x (* normalize *)
+    | _ -> make st (Term_cell.lra l)
 
   (* might need to tranfer the negation from [t] to [sign] *)
   let abs tst t : t * bool = match view t with
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 98ca0f5f..b8648684 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -304,9 +304,13 @@ end)
 
 module Th_lra = Sidekick_lra.Make(struct
   module S = Solver
+  module T = BT.Term
   type term = S.T.Term.t
 
-  include Lra
+  let mk_lra = T.lra
+  let view_as_lra t = match T.view t with
+    | T.LRA l -> l
+    | _ -> LRA_other t
 
   module Gensym = struct
     type t = {
diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml
index a6a83dc7..6ac90497 100644
--- a/src/smtlib/Typecheck.ml
+++ b/src/smtlib/Typecheck.ml
@@ -105,6 +105,21 @@ let is_num s =
   then CCString.for_all is_digit_or_dot (String.sub s 1 (String.length s-1))
   else CCString.for_all is_digit_or_dot s
 
+let string_as_q (s:string) : Q.t option =
+  try
+    let x =
+      try Q.of_string s
+      with _ ->
+        let f = float_of_string s in
+        Q.of_float f
+    in
+    Some x
+  with _ -> None
+
+let t_as_q t = match Term.view t with
+  | T.LRA (LRA_const n) -> Some n
+  | _ -> None
+
 (* conversion of terms *)
 let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
   let tst = ctx.Ctx.tst in
@@ -112,8 +127,11 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
   | PA.True -> T.true_ tst
   | PA.False -> T.false_ tst
   | PA.Const s when is_num s ->
-    errorf_ctx ctx "cannot handle numbers for now"
-    (* FIXME   A.num_str Ty.rat s (* numeral *) *)
+    let open Base_types in
+    begin match string_as_q s with
+      | Some n -> T.lra tst (LRA_const n)
+      | None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t
+    end
   | PA.Const f
   | PA.App (f, []) ->
     (* lookup in `let` table, then in type defs *)
@@ -251,8 +269,33 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
      in
      A.match_ lhs cases
        *)
-  | PA.Arith (_op, _l) ->
-    errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t
+  | PA.Arith (op, l) ->
+    let l = List.map (conv_term ctx) l in
+    let open Base_types in
+    begin match op, l with
+      | PA.Leq, [a;b] -> T.lra ctx.tst (LRA_pred (Leq, a, b))
+      | PA.Lt, [a;b] -> T.lra ctx.tst (LRA_pred (Lt, a, b))
+      | PA.Geq, [a;b] -> T.lra ctx.tst (LRA_pred (Geq, a, b))
+      | PA.Gt, [a;b] -> T.lra ctx.tst (LRA_pred (Gt, a, b))
+      | PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b))
+      | PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b))
+      | PA.Mult, [a;b] ->
+        begin match t_as_q a, t_as_q b with
+          | Some a, _ -> T.lra ctx.tst (LRA_mult (a, b))
+          | _, Some b -> T.lra ctx.tst (LRA_mult (b, a))
+          | None, None ->
+            errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t
+        end
+      | PA.Div, [a;b] ->
+        begin match t_as_q a, t_as_q b with
+          | Some a, _ -> T.lra ctx.tst (LRA_mult (Q.inv a, b))
+          | _, Some b -> T.lra ctx.tst (LRA_mult (Q.inv b, a))
+          | None, None ->
+            errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t
+        end
+      | _ ->
+        errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t
+    end;
       (* FIXME: arith
     let l = List.map (conv_term ctx) l in
     List.iter
diff --git a/src/smtlib/lra.ml b/src/smtlib/lra.ml
deleted file mode 100644
index 99e681e1..00000000
--- a/src/smtlib/lra.ml
+++ /dev/null
@@ -1,23 +0,0 @@
-
-open Sidekick_base_term
-module T = Sidekick_base_term.Term
-
-let id_leq = ID.make "<="
-let id_lt = ID.make "<"
-let id_plus = ID.make "+"
-let id_uminus = ID.make "-"
-let id_mult = ID.make "*"
-
-let fun_leq = Fun.mk_undef id_leq Ty.(Fun.mk [real; real] bool)
-let fun_lt = Fun.mk_undef id_lt Ty.(Fun.mk [real; real] bool)
-let fun_plus = Fun.mk_undef id_plus Ty.(Fun.mk [real; real] real)
-let fun_uminus = Fun.mk_undef id_plus Ty.(Fun.mk [real] real)
-let fun_times = Fun.mk_undef id_plus Ty.(Fun.mk [real; real] real)
-
-let leq st a b = T.app_fun st fun_leq (IArray.of_array_unsafe [|a; b|])
-let lt st a b = T.app_fun st fun_lt (IArray.of_array_unsafe [|a; b|])
-let lt st a b = T.app_fun st fun_lt (IArray.of_array_unsafe [|a; b|])
-
-let view_as_lra _ = assert false (* TODO *)
-
-let mk_lra _ = assert false
diff --git a/src/th-lra/Sidekick_lra.ml b/src/th-lra/Sidekick_lra.ml
index fd03bd2e..3d2472d6 100644
--- a/src/th-lra/Sidekick_lra.ml
+++ b/src/th-lra/Sidekick_lra.ml
@@ -12,6 +12,7 @@ type op = Plus | Minus
 type 'a lra_view =
   | LRA_pred of pred * 'a * 'a
   | LRA_op of op * 'a * 'a
+  | LRA_mult of Q.t * 'a
   | LRA_const of Q.t
   | LRA_other of 'a
 
@@ -19,6 +20,7 @@ let map_view f (l:_ lra_view) : _ lra_view =
   begin match l with
     | LRA_pred (p, a, b) -> LRA_pred (p, f a, f b)
     | LRA_op (p, a, b) -> LRA_op (p, f a, f b)
+    | LRA_mult (n,a) -> LRA_mult (n, f a)
     | LRA_const q -> LRA_const q
     | LRA_other x -> LRA_other (f x)
   end
@@ -163,18 +165,30 @@ module Make(A : ARG) : S with module A = A = struct
         | Plus -> t1 + t2
         | Minus -> t1 - t2
       end
+    | LRA_mult (n, x) ->
+      let t = as_linexp x in
+      LE.( n * t )
     | LRA_const q -> LE.of_const q
 
+  (* TODO: keep the linexps until they're asserted;
+     TODO: but use simplification in preprocess
+     *)
+
+
   (* preprocess linear expressions away *)
   let preproc_lra self si ~mk_lit ~add_clause (t:T.t) : T.t option =
     let _tst = SI.tst si in
     match A.view_as_lra t with
     | LRA_pred (_pre, _t1, _t2) ->
-      assert false (* TODO: define a bool variable *)
-    | LRA_op _ | LRA_const _ ->
+      None (* TODO: define a bool variable *)
+    | LRA_op _ | LRA_const _ -> None
+      (* TODO: remove?
       let le = as_linexp t in
       let proxy = fresh_term self ~pre:"lra" (T.ty t) in
       Simplex.add_eq self.simplex (V_t proxy, []); (* TODO add LE *)
+      Some proxy
+         *)
+
       (* TODO: useless?
       add_clause [
         mk_lit
@@ -182,7 +196,6 @@ module Make(A : ARG) : S with module A = A = struct
              (LRA_pred (Eq, le, Simplex.L.Comb.monomial1 (V_t proxy))))
       ];
          *)
-      Some proxy
         (*
     | B_ite (a,b,c) ->
       let t_a = fresh_term self ~pre:"ite" (T.ty b) in
@@ -191,8 +204,9 @@ module Make(A : ARG) : S with module A = A = struct
       add_clause [lit_a; mk_lit (eq self.tst t_a c)];
       Some t_a
            *)
+    | LRA_mult _ -> None (* TODO *)
     | LRA_const _ ->
-      assert false (* TODO: turn into linexp *)
+      None (* TODO: turn into linexp *)
     | LRA_other _ -> None
 
   (* TODO: remove