From a2eab9fb3c82beb531437c05e9f7d354f8858c31 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Jun 2022 10:20:14 -0500 Subject: [PATCH] Add str.unit to LFSC signature (#8862) Fixes buildbot failure. --- proofs/lfsc/signatures/theory_def.plf | 2 ++ 1 file changed, 2 insertions(+) diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf index df0abe395..04ac320ae 100644 --- a/proofs/lfsc/signatures/theory_def.plf +++ b/proofs/lfsc/signatures/theory_def.plf @@ -170,6 +170,8 @@ (define str.suffixof (# x term (# y term (apply (apply f_str.suffixof x) y)))) (declare f_str.rev term) (define str.rev (# x term (apply f_str.rev x))) +(declare f_str.unit term) +(define str.unit (# x term (apply f_str.unit x))) (declare f_str.update term) (define str.update (# x term (# y term (# z term (apply (apply (apply f_str.update x) y) z))))) (declare f_str.to_lower term) -- 2.30.2