Promote tests

I also add another tests to check if the counter increases properly.

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)
   )

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

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)
 )

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)

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)
+)

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)

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)))
 )