From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 2 Oct 2020 12:26:28 +0000 (-0700)
Subject: Remove duplicate declarations in th_bv.plf (#5183)
X-Git-Tag: cvc5-1.0.0~2768
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=16c772966206835c7f380e3a926e51af75ec3584;p=cvc5.git

Remove duplicate declarations in th_bv.plf (#5183)

I think this is dead code now, but still good to fix.
---

diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf
index 934951a86..f0ced51c7 100644
--- a/proofs/signatures/th_bv.plf
+++ b/proofs/signatures/th_bv.plf
@@ -72,7 +72,6 @@
 
 (declare bvand bvop2)
 (declare bvor bvop2)
-(declare bvor bvop2)
 (declare bvxor bvop2)
 (declare bvnand bvop2)
 (declare bvnor bvop2)
@@ -88,7 +87,6 @@
 (declare bvshl bvop2)
 (declare bvlshr bvop2)
 (declare bvashr bvop2)
-(declare concat bvop2)
 
 ; bit vector unary operators
 (define bvop1