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.

diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf
index 6454de2fd9654202a87ea18ab0945e54a796cf21..0049d6232863387847a11651d2725908ac4f4226 100644 (file)
--- 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