From a10737cfa028daf0ed0011bf2ee27a8cfe138eea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Wed, 12 Jul 2023 10:06:13 +0000 Subject: [PATCH] Promote cram.t with new model format (#734) --- tests/cram.t/run.t | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 223284b71..f0553f8e1 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -12,9 +12,10 @@ appropriate here. unknown ( + (define-fun a1 () (Array Int Int) + (store ((as const (Array Int Int)) 0) 0 0)) (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) ) Now we will test some semantic triggers.