diff --git a/.travis.yml b/.travis.yml
index 746d014c..d666743d 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -5,11 +5,13 @@ services:
 - docker
 env:
   global:
-  - PINS="sidekick:. sidekick-bin:."
+    - PINS="sidekick:. sidekick-arith:. sidekick-bin:."
   - DISTRO="ubuntu-16.04"
   matrix:
   - PACKAGE="sidekick" CAML_VERSION="4.03"
   - PACKAGE="sidekick" CAML_VERSION="4.06"
   - PACKAGE="sidekick" CAML_VERSION="4.08"
   - PACKAGE="sidekick" CAML_VERSION="4.10"
+  - PACKAGE="sidekick-arith" CAML_VERSION="4.03"
+  - PACKAGE="sidekick-arith" CAML_VERSION="4.10"
   - PACKAGE="sidekick-bin" CAML_VERSION="4.06"
diff --git a/sidekick-arith.opam b/sidekick-arith.opam
new file mode 100644
index 00000000..2dff41c1
--- /dev/null
+++ b/sidekick-arith.opam
@@ -0,0 +1,25 @@
+opam-version: "2.0"
+name: "sidekick"
+license: "Apache"
+synopsis: "SMT solver based on msat and CDCL(T) (functor library)"
+version: "dev"
+author: ["Simon Cruanes"]
+maintainer: ["simon.cruanes.2007@m4x.org"]
+build: [
+  ["dune" "build" "@install" "-p" name "-j" jobs]
+  ["dune" "build" "@doc" "-p" name "-j" jobs ] {with-doc}
+  ["dune" "runtest" "-p" name "-j" jobs] {with-test}
+]
+depends: [
+  "dune" { >= "1.1" }
+  "containers" { >= "3.0" & < "4.0" }
+  "iter" { >= "1.0" & < "2.0" }
+  "ocaml" { >= "4.03" }
+  "zarith"
+  "alcotest" {with-test}
+]
+tags: [ "sat" "smt" ]
+homepage: "https://github.com/c-cube/sidekick"
+dev-repo: "git+https://github.com/c-cube/sidekick.git"
+bug-reports: "https://github.com/c-cube/sidekick/issues/"
+
diff --git a/src/th-lra/Sidekick_lra.ml b/src/arith/lra/Sidekick_arith_lra.ml
similarity index 100%
rename from src/th-lra/Sidekick_lra.ml
rename to src/arith/lra/Sidekick_arith_lra.ml
diff --git a/src/th-lra/dune b/src/arith/lra/dune
similarity index 70%
rename from src/th-lra/dune
rename to src/arith/lra/dune
index cdab035a..efe280aa 100644
--- a/src/th-lra/dune
+++ b/src/arith/lra/dune
@@ -1,7 +1,7 @@
 
 (library
-  (name sidekick_lra)
-  (public_name sidekick.th-lra)
+  (name sidekick_arith_lra)
+  (public_name sidekick-arith.lra)
   (optional) ; only if deps present
   (flags :standard -warn-error -a+8 -open Sidekick_util)
   (libraries containers sidekick.core zarith))
diff --git a/src/th-lra/fourier_motzkin.ml b/src/arith/lra/fourier_motzkin.ml
similarity index 100%
rename from src/th-lra/fourier_motzkin.ml
rename to src/arith/lra/fourier_motzkin.ml
diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml
index f86f3be4..dd60dc5d 100644
--- a/src/base-term/Base_types.ml
+++ b/src/base-term/Base_types.ml
@@ -4,10 +4,10 @@ module Fmt = CCFormat
 
 module CC_view = Sidekick_core.CC_view
 
-type lra_pred = Sidekick_lra.FM.Pred.t = Lt | Leq | Geq | Gt | Neq | Eq
-type lra_op = Sidekick_lra.op = Plus | Minus
+type lra_pred = Sidekick_arith_lra.FM.Pred.t = Lt | Leq | Geq | Gt | Neq | Eq
+type lra_op = Sidekick_arith_lra.op = Plus | Minus
 
-type 'a lra_view = 'a Sidekick_lra.lra_view =
+type 'a lra_view = 'a Sidekick_arith_lra.lra_view =
   | LRA_pred of lra_pred * 'a * 'a
   | LRA_op of lra_op * 'a * 'a
   | LRA_mult of Q.t * 'a
@@ -726,7 +726,7 @@ end = struct
     | Not u -> Not (f u)
     | Eq (a,b) -> Eq (f a, f b)
     | Ite (a,b,c) -> Ite (f a, f b, f c)
-    | LRA l -> LRA (Sidekick_lra.map_view f l)
+    | LRA l -> LRA (Sidekick_arith_lra.map_view f l)
 
   module Tbl = CCHashtbl.Make(struct
       type t = term view
@@ -964,7 +964,7 @@ end = struct
     | Not u -> not_ tst (f u)
     | Eq (a,b) -> eq tst (f a) (f b)
     | Ite (a,b,c) -> ite tst (f a) (f b) (f c)
-    | LRA l -> lra tst (Sidekick_lra.map_view f l)
+    | LRA l -> lra tst (Sidekick_arith_lra.map_view f l)
 end
 
 module Value : sig
diff --git a/src/base-term/dune b/src/base-term/dune
index c056f5ae..286c652d 100644
--- a/src/base-term/dune
+++ b/src/base-term/dune
@@ -2,5 +2,5 @@
  (name sidekick_base_term)
  (public_name sidekick.base-term)
  (synopsis "Basic term definitions for the standalone SMT solver")
- (libraries containers sidekick.core sidekick.util sidekick.th-lra zarith)
+ (libraries containers sidekick.core sidekick.util sidekick-arith.lra zarith)
  (flags :standard -w -32 -open Sidekick_util))
diff --git a/src/cc/dune b/src/cc/dune
index 9f98727a..d86f371f 100644
--- a/src/cc/dune
+++ b/src/cc/dune
@@ -4,4 +4,4 @@
   (name Sidekick_cc)
   (public_name sidekick.cc)
   (libraries containers iter sidekick.core sidekick.util)
-  (flags :standard -warn-error -a+8 -open Sidekick_util))
+  (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util))
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index c0789be9..3ae64420 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -302,7 +302,7 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
   include Form
 end)
 
-module Th_lra = Sidekick_lra.Make(struct
+module Th_lra = Sidekick_arith_lra.Make(struct
   module S = Solver
   module T = BT.Term
   type term = S.T.Term.t
diff --git a/src/smtlib/dune b/src/smtlib/dune
index b87df1c5..2481585f 100644
--- a/src/smtlib/dune
+++ b/src/smtlib/dune
@@ -3,7 +3,5 @@
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith msat sidekick.core sidekick.util
    sidekick.msat-solver sidekick.base-term sidekick.th-bool-static
-   sidekick.mini-cc sidekick.th-data sidekick.th-lra msat.backend smtlib-utils)
+   sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils)
  (flags :standard -warn-error -a+8 -open Sidekick_util))
-
-; TODO: enable warn-error again