diff --git a/doc/guide.md b/doc/guide.md
index bb002450..63b6ef9d 100644
--- a/doc/guide.md
+++ b/doc/guide.md
@@ -347,9 +347,7 @@ Sidekick_base_solver.Solver.Sat
   (a := 0)
   (b := 0)
   ((<= (+ a (* -1 b)) 0) := true)
-  (_sk_lra__le_comb0 := 0)
-  ((= a b) := true)
-  ((>= (+ a (* -1 b)) 0) := true))
+  (_sk_lra__le_comb0 := 0))
 
 
 # let a_geq_1 = Term.LRA.(geq tstore a (const tstore (Q.of_int 1)));;
diff --git a/src/tests/regression/reg_model_lra1.out.expected b/src/tests/regression/reg_model_lra1.out.expected
index 7a2ad496..1f30f689 100644
--- a/src/tests/regression/reg_model_lra1.out.expected
+++ b/src/tests/regression/reg_model_lra1.out.expected
@@ -2,8 +2,8 @@
  (true := true) 
  (false := false) 
  (a := 5/3) 
- ((* 3 a) := 5) 
- (5 := 5) 
+ ((* 3 a) := 0) 
+ (5 := 0) 
  ((= (* 3 a) 5) := true) 
  ((<= (* 3 a) 5) := true) 
  ((>= (* 3 a) 5) := true))