summaryrefslogtreecommitdiff
path: root/proofs/signatures/th_bv_bitblast.plf
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/signatures/th_bv_bitblast.plf')
-rw-r--r--proofs/signatures/th_bv_bitblast.plf2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf
index 2b2fe0868..109155a21 100644
--- a/proofs/signatures/th_bv_bitblast.plf
+++ b/proofs/signatures/th_bv_bitblast.plf
@@ -173,7 +173,7 @@
(! xb bblt
(! rb bblt
(! xbb (bblast_term m x xb)
- (! c ( ^ (bblast_sextend xb k m) rb)
+ (! c ( ^ (bblast_sextend xb k) rb)
(bblast_term n (sign_extend n k m x) rb))))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback