From 6de1f210e9565d3cb4b5761519479d64cdd77706 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 12 Jan 2022 13:51:00 +0100
Subject: [PATCH] [WP] fixes eq_sequence
---
src/plugins/wp/Vlist.ml | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 398519e13df..2f5b218cdb2 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -262,7 +262,6 @@ let rec subsequence xs rs ys =
let rs,ys = omit rs x ys in
subsequence xs rs ys
-let p_is_nil a = F.p_equal a (v_nil (F.typeof a))
let rewrite_eq a b =
match F.repr a , F.repr b with
| L.Fun(nil,[]) , _ when nil == f_nil -> rewrite_is_nil ~nil:a b
@@ -272,9 +271,14 @@ let rewrite_eq a b =
try rightmost_eq a b with Not_found ->
let xs = elements a in
let ys = elements b in
- if List.length xs < List.length ys
- then F.p_all p_is_nil (subsequence xs [] ys)
- else F.p_all p_is_nil (subsequence ys [] xs)
+ let rs = if List.length xs < List.length ys
+ then subsequence xs [] ys
+ else subsequence ys [] xs
+ in
+ let pred = F.p_all (fun s -> F.p_equal s (v_nil (F.typeof s))) rs in
+ if F.decide (e_prop pred)
+ then F.p_true
+ else raise Not_found
(* All Simplifications *)
--
GitLab