diff --git a/non-regression/non-regression.sh b/non-regression/non-regression.sh
index 2b59b6eb8b..b070176f8e 100755
--- a/non-regression/non-regression.sh
+++ b/non-regression/non-regression.sh
@@ -23,5 +23,5 @@ echo "==========================================================================
 echo "[ WITH FM-SIMPLEX ]"
 echo "===============================================================================================";
 echo "===============================================================================================";
-./main_script.sh "-inequalities-plugin `pwd`/../sources/_build/install/default/fm-simplex-plugin.cmxs"
+./main_script.sh "-inequalities-plugin `pwd`/../sources/_build/install/default/share/plugins/fm-simplex-plugin.cmxs"
 
diff --git a/sources/lib/dune b/sources/lib/dune
index d82b766f01..e8c0e1029f 100644
--- a/sources/lib/dune
+++ b/sources/lib/dune
@@ -13,16 +13,16 @@
   ; modules that make up the lib
   (modules
     ; frontend
-    Cnf Frontend Parsed_interface Triggers Typechecker
+    Cnf Frontend Parsed_interface Typechecker
     ; reasoners
     Ac Arith Arrays Bitv Ccx Combine Enum Fun_sat Inequalities
     Instances IntervalCalculus Intervals Ite Matching Matching_types
     Polynome Records Satml_frontend_hybrid Satml_frontend Satml
     Sat_solver Sat_solver_sig Sig Theory Uf Use
     ; structures
-    Commands Errors Exception Explanation Formula Fpa_rounding
-    Literal Parsed Profiling Satml_types Symbols
-    Term Tliteral Ty Typed
+    Commands Errors Exception Explanation Fpa_rounding
+    Parsed Profiling Satml_types Symbols
+    Expr Var Ty Typed Xliteral
     ; util
     Config Emap Gc_debug Hconsing Hstring Iheap Lists Loc
     MyDynlink MyUnix Numbers NumsNumbers NumbersInterface