Add tests

OCamlPro · Jun 29, 2023 · 14ebcf9 · 14ebcf9
1 parent a588a7a
commit 14ebcf9
Show file tree

Hide file tree

Showing 8 changed files with 29 additions and 80 deletions.
diff --git a/tests/issues/555/models/555.expected b/tests/issues/555/models/555.expected
@@ -0,0 +1,7 @@
+
+unknown
+(
+  (define-fun x () Int 0)
+  (define-fun y () Int 0)
+  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
+)
diff --git a/tests/issues/555/models/555.smt2 b/tests/issues/555/models/555.smt2
@@ -0,0 +1,10 @@
+(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))
+(check-sat)
+(get-model)
diff --git a/tests/models/arith/arith1.expected b/tests/models/arith/arith1.expected
@@ -1,14 +1,5 @@
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
-(define-fun x () Int 0)
-
- ; Arrays not yet supported
-
-
+  (define-fun x () Int 0)
 )
diff --git a/tests/models/arith/arith2.expected b/tests/models/arith/arith2.expected
@@ -1,16 +1,6 @@
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
-(define-fun x () Int 8)
-
-(define-fun y () Int 42)
-
- ; Arrays not yet supported
-
-
+  (define-fun x () Int 8)
+  (define-fun y () Int 42)
 )
diff --git a/tests/models/bool/bool1.expected b/tests/models/bool/bool1.expected
@@ -1,30 +1,11 @@
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
- ; Arrays not yet supported
-
-
 )
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
-(define-fun p () Bool true)
-
-(define-fun q () Bool true)
-
-(define-fun nq () Bool true)
-
- ; Arrays not yet supported
-
-
+  (define-fun p () Bool true)
+  (define-fun q () Bool true)
+  (define-fun nq () Bool true)
 )
diff --git a/tests/models/bool/bool2.expected b/tests/models/bool/bool2.expected
@@ -1,12 +1,4 @@
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
- ; Arrays not yet supported
-
-
 )
diff --git a/tests/models/uf/uf1.expected b/tests/models/uf/uf1.expected
@@ -1,18 +1,7 @@
 
 unknown
 (
-
- ; Functions
-
-(define-fun f ((arg_0 Int)) Int 0)
-
- ; Constants
-
-(define-fun a () Int 0)
-
-(define-fun b () Int 0)
-
- ; Arrays not yet supported
-
-
+  (define-fun f ((arg_0 Int)) Int 0)
+  (define-fun a () Int 0)
+  (define-fun b () Int 0)
 )
diff --git a/tests/models/uf/uf2.expected b/tests/models/uf/uf2.expected
@@ -1,18 +1,7 @@
 
 unknown
 (
-
- ; Functions
-
-(define-fun f ((arg_0 Int)) Int (ite (= arg_0 a) 2 0))
-
- ; Constants
-
-(define-fun a () Int 0)
-
-(define-fun b () Int (- 2))
-
- ; Arrays not yet supported
-
-
+  (define-fun f ((arg_0 Int)) Int (ite (= arg_0 a) 2 0))
+  (define-fun a () Int 0)
+  (define-fun b () Int (- 2))
 )