From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 7 Jun 2022 15:20:14 +0000 (-0500)
Subject: Add str.unit to LFSC signature (#8862)
X-Git-Tag: cvc5-1.0.1~62
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a2eab9fb3c82beb531437c05e9f7d354f8858c31;p=cvc5.git

Add str.unit to LFSC signature (#8862)

Fixes buildbot failure.
---

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)