From 97094a32222a731c4828432a1383fdda68993f22 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Mon, 25 Sep 2023 11:55:04 +0200
Subject: [PATCH] Promote tests

I also add another tests to check if the counter increases properly.
---
 tests/cram.t/run.t                           |  2 +-
 tests/dune.inc                               | 26 ++++++++++++++++++++
 tests/issues/555.models.expected             |  3 ++-
 tests/issues/555.models.smt2                 |  2 ++
 tests/models/array/array1.models.expected    |  8 ++++++
 tests/models/array/array1.models.smt2        | 12 +++++++++
 tests/models/records/record1.models.expected |  2 +-
 7 files changed, 52 insertions(+), 3 deletions(-)
 create mode 100644 tests/models/array/array1.models.expected
 create mode 100644 tests/models/array/array1.models.smt2

diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index 3f573aa7f..3839345ac 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -10,7 +10,7 @@ appropriate here.
   
   unknown
   (
-    (define-fun a1 () (Array Int Int) (store (as @!k1 (Array Int Int)) 0 0))
+    (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
     (define-fun x () Int 0)
     (define-fun y () Int 0)
   )
diff --git a/tests/dune.inc b/tests/dune.inc
index b94a3f7f2..fa3c71566 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -195276,6 +195276,32 @@
 ; Auto-generated part end
 ; File auto-generated by gentests
 
+; Auto-generated part begin
+(subdir models/array
+  (rule
+   (target array1.models_tableaux.output)
+   (deps (:input array1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff array1.models.expected array1.models_tableaux.output))))
+; Auto-generated part end
+; File auto-generated by gentests
+
 ; Auto-generated part begin
 (subdir models/bool
   (rule
diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected
index b0b076c14..ef323fb3e 100644
--- a/tests/issues/555.models.expected
+++ b/tests/issues/555.models.expected
@@ -1,7 +1,8 @@
 
 unknown
 (
-  (define-fun a1 () (Array Int Int) (store (as @!k1 (Array Int Int)) 0 0))
+  (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
   (define-fun x () Int 0)
   (define-fun y () Int 0)
 )
diff --git a/tests/issues/555.models.smt2 b/tests/issues/555.models.smt2
index 49a09084c..6c9d2634f 100644
--- a/tests/issues/555.models.smt2
+++ b/tests/issues/555.models.smt2
@@ -6,5 +6,7 @@
 (declare-const a2 (Array Int Int))
 (assert (= (select a1 x) x))
 (assert (= (store a1 x y) a1))
+(assert (= (select a2 x) x))
+(assert (= (store a2 x y) a1))
 (check-sat)
 (get-model)
diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected
new file mode 100644
index 000000000..ef323fb3e
--- /dev/null
+++ b/tests/models/array/array1.models.expected
@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
+  (define-fun x () Int 0)
+  (define-fun y () Int 0)
+)
diff --git a/tests/models/array/array1.models.smt2 b/tests/models/array/array1.models.smt2
new file mode 100644
index 000000000..6c9d2634f
--- /dev/null
+++ b/tests/models/array/array1.models.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const a1 (Array Int Int))
+(declare-const a2 (Array Int Int))
+(assert (= (select a1 x) x))
+(assert (= (store a1 x y) a1))
+(assert (= (select a2 x) x))
+(assert (= (store a2 x y) a1))
+(check-sat)
+(get-model)
diff --git a/tests/models/records/record1.models.expected b/tests/models/records/record1.models.expected
index 20e26682b..c8d49e171 100644
--- a/tests/models/records/record1.models.expected
+++ b/tests/models/records/record1.models.expected
@@ -1,5 +1,5 @@
 
 unknown
 (
-  (define-fun a () Pair (pair 5 (as @!k3 Int)))
+  (define-fun a () Pair (pair 5 (as @a0 Int)))
 )