From bae2c9cd668590b731025e43e79f1dca3efc7d33 Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Tue, 22 Nov 2022 17:05:35 +0100
Subject: [PATCH] [Array] Fixed res-ext soundness error
---
colibri2/theories/array/array.ml | 11 +++++------
1 file changed, 5 insertions(+), 6 deletions(-)
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 70c34a6c4..fe6ecdde6 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -200,10 +200,9 @@ let apply_const v = apply_cst Builtin.array_const [] [ v ]
let apply_def_index a = apply_cst Builtin.array_default_index [] [ a ]
let apply_def_value a = apply_cst Builtin.array_default_value [] [ a ]
-let eq_array_diff a b =
- Expr.Term.eq
- (Expr.Term.Array.select a (apply_cst Builtin.array_diff [] [ a; b ]))
- (Expr.Term.Array.select b (apply_cst Builtin.array_diff [] [ a; b ]))
+let distinct_arrays a b =
+ let diff = apply_diff a b in
+ Expr.Term.distinct [ mk_select_term a diff; mk_select_term b diff ]
let apply_ext env a b =
let va = Expr.Term.Var.mk "a" array_ty in
@@ -378,7 +377,7 @@ module Theory = struct
| (nvar, nterm, nnode) :: t ->
let nterms =
List.fold_left
- (fun acc (_, oterm, _) -> eq_array_diff nterm oterm :: acc)
+ (fun acc (_, oterm, _) -> distinct_arrays nterm oterm :: acc)
[] t
in
aux (nterms @ terms_acc) ((nvar, nnode) :: tsubsts_acc) t
@@ -404,7 +403,7 @@ module Theory = struct
Expr.Term.Var.mk (Format.sprintf "a%d" cnt) tyvt
in
let anvt = Expr.Term.of_var anv in
- ( eq_array_diff a0vt anvt :: nterms,
+ ( distinct_arrays a0vt anvt :: nterms,
(anv, anvt, node) :: nsubsts,
cnt + 1 ))
([], [], 1) t
--
GitLab