From 595dc0f6f3efaa2f6b084bee7a57d5d399c317c7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 6 May 2022 10:48:49 -0500 Subject: [PATCH] Fix LFSC side condition for matching premise of concat_unify (#8726) Occurs in QF_SLIA/20180523-Reynolds/pyex/peterc-pyex-doc-cav17-td/pymongo/pymongo-mongoclient/cc647bd246e485aa31a4dc8978e5211a7c1336911d1bfc78b45ee679.smt2 after 464 seconds on my machine. --- proofs/lfsc/signatures/strings_rules.plf | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf index 6454de2fd..0049d6232 100644 --- a/proofs/lfsc/signatures/strings_rules.plf +++ b/proofs/lfsc/signatures/strings_rules.plf @@ -31,14 +31,21 @@ (program sc_concat_head_or_self ((s term) (s1 term) (rev flag) (u sort)) Ok (ifequal s s1 ok - (let sh (sc_string_head (sc_string_rev s rev u)) + (let ss (sc_string_rev s rev u) + (let sh (sc_string_head ss) (ifequal sh s1 ok - ; otherwise we may be splitting a constant, we reverse the characters in sh - (ifequal (sc_string_is_prefix - (sc_string_rev (sc_string_nary_intro s1 u) rev u) - (sc_string_rev sh rev u) u) - tt ok (fail Ok))))) + ; otherwise we may be splitting a constant, get s1 in n-ary form + (let s1n (sc_string_rev (sc_string_nary_intro s1 u) rev u) + ; it may be that s itself is a constant, in which case we must consider + ; it as a whole, not just its head + (ifequal (sc_string_is_prefix s1n ss u) tt + ok + ; we are splitting a constant in the head of s1, notice we must reverse + ; its characters, since they were not reversed when computing ss + (ifequal (sc_string_is_prefix s1n (sc_string_rev sh rev u) u) tt + ok + (fail Ok)))))))) ) ; Computes whether the heads of the premise (= s t) match s1 and t1 for the -- 2.30.2