From c4bbaddc06c3fb938b3f7e7c8622eed2c9b934ea Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 2 Feb 2022 16:12:55 -0500
Subject: [PATCH] new regression test for `(get-model)`; fix mdx test

---
 doc/guide.md                                     |  2 +-
 src/tests/regression/dune                        | 11 +++++++++++
 src/tests/regression/reg_model_lra1.out.expected | 11 +++++++++++
 src/tests/regression/reg_model_lra1.smt2         |  6 ++++++
 4 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 src/tests/regression/dune
 create mode 100644 src/tests/regression/reg_model_lra1.out.expected
 create mode 100644 src/tests/regression/reg_model_lra1.smt2

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)