projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 86cc730)
Remove duplicate declarations in th_bv.plf (#5183)
authorAlex Ozdemir <aozdemir@hmc.edu>
Fri, 2 Oct 2020 12:26:28 +0000 (05:26 -0700)
committerGitHub <noreply@github.com>
Fri, 2 Oct 2020 12:26:28 +0000 (07:26 -0500)
I think this is dead code now, but still good to fix.

proofs/signatures/th_bv.plf patch | blob | history

diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf
index 934951a866b06da33303973fad609a8f56fae725..f0ced51c7cc5ccc25ec30728160e275a71c0146d 100644 (file)
--- 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