diff --git a/doc/guide.md b/doc/guide.md
index 10f319cf..0477788e 100644
--- a/doc/guide.md
+++ b/doc/guide.md
@@ -344,7 +344,7 @@ Sidekick_base_solver.Solver.Sat
  (model
   (true := true)
   (false := false)
-  (_sk_lra__le0 := _sk_lra__le0)
+  (_sk_lra__le0 := 0)
   ((_sk_lra__le0 <= 0) := true))
 
 
diff --git a/src/tests/regression/dune b/src/tests/regression/dune
new file mode 100644
index 00000000..2edda42d
--- /dev/null
+++ b/src/tests/regression/dune
@@ -0,0 +1,11 @@
+
+(rule
+  (targets reg_model_lra1.out)
+  (deps reg_model_lra1.smt2)
+  (action (with-stdout-to %{targets} (bash "../../main/main.exe %{deps} | tail -n +2"))))
+
+(alias
+  (name runtest)
+  (locks /test)
+  (package sidekick-bin)
+  (action (diff reg_model_lra1.out.expected reg_model_lra1.out)))
diff --git a/src/tests/regression/reg_model_lra1.out.expected b/src/tests/regression/reg_model_lra1.out.expected
new file mode 100644
index 00000000..13fd1fb2
--- /dev/null
+++ b/src/tests/regression/reg_model_lra1.out.expected
@@ -0,0 +1,11 @@
+(model
+ (true := true) 
+ (false := false) 
+ (a := 5/3) 
+ (_sk_lra__le0 := 5) 
+ ((to_real _sk_lra__le0) := 5) 
+ ((= 5 (to_real _sk_lra__le0)) := true) 
+ (((to_real _sk_lra__le0) >= 5) := true) 
+ (((to_real _sk_lra__le0) <= 5) := true) 
+ ((a <= 5/3) := true) 
+ ((a >= 5/3) := true))
diff --git a/src/tests/regression/reg_model_lra1.smt2 b/src/tests/regression/reg_model_lra1.smt2
new file mode 100644
index 00000000..eef1d2b1
--- /dev/null
+++ b/src/tests/regression/reg_model_lra1.smt2
@@ -0,0 +1,6 @@
+
+(set-logic QF_LRA)
+(declare-const a Real)
+(assert (= (* 3 a) 5))
+(check-sat)
+(get-model)