diff --git a/drivers/smt-libv2.drv b/drivers/smt-libv2.drv
index 749e473c25ba28bc0bfbfd8c86fd0d674cbc4fe9..e132d46fcdf9463c8cd9ffba340d83b5a0f2ac23 100644
--- a/drivers/smt-libv2.drv
+++ b/drivers/smt-libv2.drv
@@ -200,7 +200,7 @@ theory bv.BV32
   (* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *)
   (* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *)
   syntax predicate eq "(= %1 %2)"
-  remove prop Equationality
+  remove prop Extensionality
 
   syntax predicate slt "(bvslt %1 %2)"
   syntax predicate sle "(bvsle %1 %2)"