Make LFSC side condition for concat unify robust to equality with full string (#8028)

Was leading to LFSC proof checking failures.

diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf
index af981096a72e35ef0a501e3bca9a6c2bfbc4fde7..3439500b2abbeb8a9c2045680591c843de8bc9c3 100644 (file)
--- a/proofs/lfsc/signatures/strings_rules.plf
+++ b/proofs/lfsc/signatures/strings_rules.plf
@@ -20,11 +20,21 @@
                    (! r (^ (sc_concat_eq s t rev) res) 
                       (holds res))))))))
 
+; Helper method for PfRule::CONCAT_UNIFY. Returns ok if s or its head is equal to s1,
+; where the head of the reverse of s is checked if rev is tt. Fails otherwise.
+(program sc_concat_head_or_self ((s term) (s1 term) (rev flag)) Ok
+  (ifequal s s1
+    ok
+    (ifequal (sc_string_head (sc_string_rev s rev)) s1
+      ok
+      (fail Ok)))
+)
+
 ; Computes whether the heads of the premise (= s t) match s1 and t1 for the
 ; PfRule::CONCAT_UNIFY rule
 (program sc_concat_unify ((s term) (t term) (s1 term) (t1 term) (rev flag)) Ok
-  (ifequal (sc_string_head (sc_string_rev s rev)) s1
-    (ifequal (sc_string_head (sc_string_rev t rev)) t1
+  (ifequal (sc_concat_head_or_self s s1 rev) ok
+    (ifequal (sc_concat_head_or_self t t1 rev) ok
       ok
       (fail Ok))
     (fail Ok)))

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index aded275b6582e563017c91b02d1f2993d0cedf3b..72d8b0cc948c79783249c9a7d3040a8489639cd9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2437,6 +2437,7 @@ set(regress_1_tests
   regress1/strings/regexp001.smt2
   regress1/strings/regexp002.smt2
   regress1/strings/regexp003.smt2
+  regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2
   regress1/strings/regexp-strat-fix.smt2
   regress1/strings/reloop.smt2
   regress1/strings/repl-empty-sem.smt2

diff --git a/test/regress/regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2 b/test/regress/regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2
new file mode 100644 (file)
index 0000000..f453d93
--- /dev/null
+++ b/test/regress/regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const y String)
+(assert (= 2 (str.len y)))
+(assert (str.in_re y (re.+ (re.range "!" "3"))))
+(assert (str.contains "1kN" y))
+(check-sat)