From a4668747c780ac55f0d2d84cbc144de07a92c586 Mon Sep 17 00:00:00 2001 From: Basile Clement Date: Wed, 12 Jul 2023 11:02:17 +0200 Subject: [PATCH] Promote cram.t with new model format --- 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.