Update of bitvector modules and tests, syncing with what was done within spark repository.

drivers/cvc4_bare.drv

@@ -32,3 +32,265 @@ theory int.ComputerDivision
    remove prop Div_1
 end
 *)
+
+(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
+   have the same name for the function to_int *)
+theory bitvec.BitVector64
+  syntax type t "(_ BitVec 64)"
+
+  syntax function zero "#x00000000"
+  syntax function ones "#xFFFFFFFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 64)"
+  syntax function to_int "(bv2nat %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+end
+
+theory bitvec.BitVector32
+  syntax type t "(_ BitVec 32)"
+
+  syntax function zero "#x00000000"
+  syntax function ones "#xFFFFFFFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 32)"
+  syntax function to_int "(bv2nat %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+end
+
+theory bitvec.BitVector16
+  syntax type t "(_ BitVec 16)"
+
+  syntax function zero "#x0000"
+  syntax function ones "#xFFFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 16)"
+  syntax function to_int "(bv2nat %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+end
+
+theory bitvec.BitVector8
+  syntax type t "(_ BitVec 8)"
+
+  syntax function zero "#x00"
+  syntax function ones "#xFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 8)"
+  syntax function to_int "(bv2nat %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 8)) (_ bv0 8)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
+end

drivers/smt-libv2.drv

-(* Why driver for SMT-lib v2 syntax *)
+(* Why driver for SMTLIB2 syntax *)
 
 prelude ";;; this is a prelude for smt-lib v2"
-(*prelude "(set-logic AUFNIRA)"*)
-(** A  : Array
-    UF : Uninterpreted Function
-    DT : Datatypes (not needed at the end ...)
-    NIRA : NonLinear Integer Reals Arithmetic
-*)
 
 printer "smtv2"
 filename "%f-%t-%g.smt2"
-
 valid "^unsat"
 unknown "^\\(unknown\\|sat\\|Fail\\)" ""
 outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
@@ -49,7 +42,7 @@ theory int.Int
 
   syntax function (+)  "(+ %1 %2)"
   syntax function (-)  "(- %1 %2)"
-  syntax function (*)  "(* %1 %2)"
+  syntax function ( * )  "(* %1 %2)"
   syntax function (-_) "(- %1)"
 
   syntax predicate (<=) "(<= %1 %2)"
@@ -78,7 +71,6 @@ theory int.Int
 
 end
 
-
 theory real.Real
 
   prelude ";;; this is a prelude for smt-lib v2 real arithmetic"
@@ -88,7 +80,7 @@ theory real.Real
 
   syntax function (+)  "(+ %1 %2)"
   syntax function (-)  "(- %1 %2)"
-  syntax function (*)  "(* %1 %2)"
+  syntax function ( * )  "(* %1 %2)"
   syntax function (/)  "(/ %1 %2)"
   syntax function (-_) "(- %1)"
   syntax function inv  "(/ 1.0 %1)"
@@ -161,50 +153,37 @@ theory map.Map
 (*  syntax function const "(const[%t0] %1)" *)
 end
 
-theory bv.BV32
-  syntax type t "(_ BitVec 32)"
+theory bitvec.BVConverter_32_64
+  syntax function toBig "((_ zero_extend 32) %1)"
+  syntax function toSmall "((_ extract 31 0) %1)"
+end
 
-  syntax function zero "#x00000000"
-  syntax function ones "#xFFFFFFFF"
-  syntax function bw_and "(bvand %1 %2)"
-  syntax function bw_or "(bvor %1 %2)"
-  syntax function bw_xor "(bvxor %1 %2)"
-  syntax function bw_not "(bvnot %1)"
+theory bitvec.BVConverter_16_64
+  syntax function toBig "((_ zero_extend 48) %1)"
+  syntax function toSmall "((_ extract 15 0) %1)"
+end
 
-  syntax function add "(bvadd %1 %2)"
-  syntax function sub "(bvsub %1 %2)"
-  syntax function neg "(bvneg %1)"
-  syntax function mul "(bvmul %1 %2)"
-  syntax function udiv "(bvudiv %1 %2)"
-  syntax function urem "(bvurem %1 %2)"
-  syntax function sdiv "(bvsdiv %1 %2)"
-  syntax function srem "(bvsrem %1 %2)"
-  syntax function smod "(bvsmod %1 %2)"
+theory bitvec.BVConverter_8_64
+  syntax function toBig "((_ zero_extend 56) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
+end
 
-  syntax function rotate_left "((_ rotate_left 1) %1)"
-  syntax function rotate_right "((_ rotate_right 1) %1)"
+theory bitvec.BVConverter_16_32
+  syntax function toBig "((_ zero_extend 16) %1)"
+  syntax function toSmall "((_ extract 15 0) %1)"
+end
 
-  syntax function lsr "(bvlshr %1 ((_ int2bv 32) %2))"
-  syntax function lsl "(bvshl %1 ((_ int2bv 32) %2))"
-  syntax function asr "(bvashr %1 ((_ int2bv 32) %2))"
-  syntax function lsr_bv "(bvlshr %1 %2)"
-  syntax function lsl_bv "(bvshl %1 %2)"
-  syntax function asr_bv "(bvashr %1 %2)"
-  syntax converter of_int_const "((_ int2bv 32) %1)"
-  syntax predicate eq "(= %1 %2)"
-  remove prop Extensionality
+theory bitvec.BVConverter_8_32
+  syntax function toBig "((_ zero_extend 24) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
+end
 
-  syntax predicate slt "(bvslt %1 %2)"
-  syntax predicate sle "(bvsle %1 %2)"
-  syntax predicate sgt "(bvsgt %1 %2)"
-  syntax predicate sge "(bvsge %1 %2)"
-  syntax predicate ult "(bvult %1 %2)"
-  syntax predicate ule "(bvule %1 %2)"
-  syntax predicate ugt "(bvugt %1 %2)"
-  syntax predicate uge "(bvuge %1 %2)"
+theory bitvec.BVConverter_8_16
+  syntax function toBig "((_ zero_extend 8) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
 end
 
-theory bv.BV32Ax
+theory bv.BV32
   syntax type t "(_ BitVec 32)"
 
   syntax function zero "#x00000000"
@@ -235,6 +214,7 @@ theory bv.BV32Ax
   syntax function asr_bv "(bvashr %1 %2)"
   syntax converter of_int_const "((_ int2bv 32) %1)"
   syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
 
   syntax predicate slt "(bvslt %1 %2)"
   syntax predicate sle "(bvsle %1 %2)"
@@ -244,12 +224,6 @@ theory bv.BV32Ax
   syntax predicate ule "(bvule %1 %2)"
   syntax predicate ugt "(bvugt %1 %2)"
   syntax predicate uge "(bvuge %1 %2)"
-
-  remove prop Add_is_add
-  remove prop Min_is_min
-  remove prop Neg_is_neg
-  remove prop Mul_is_mul
-  remove prop Udiv_is_udiv
 end
 
 theory bv.BV64
@@ -379,7 +353,6 @@ theory bv.BV8
 end
 
 theory bv.BVConverter_32_64
-  (* syntax function toBig "(concat #x00000000 %1)" *)
   syntax function toBig "((_ zero_extend 32) %1)"
   syntax function toSmall "((_ extract 31 0) %1)"
 
@@ -394,7 +367,7 @@ theory bv.BVConverter_16_64
 end
 
 theory bv.BVConverter_8_64
-  syntax function toBig "((_ zero_extend 54) %1)"
+  syntax function toBig "((_ zero_extend 56) %1)"
   syntax function toSmall "((_ extract 7 0) %1)"
 
   remove prop back_from_bigBV

drivers/z3_bare.drv

@@ -20,7 +20,7 @@ theory real.FromInt
   remove prop Neg
 end
 
-(* does not work: Z3 segfaults 
+(* does not work: Z3 segfaults
 theory real.Trigonometry
 
   syntax function cos "(cos %1)"
@@ -32,4 +32,266 @@ theory real.Trigonometry
 end
 *)
 
-import "discrimination.gen"
\ No newline at end of file
+import "discrimination.gen"
+
+(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
+   have the same name for the function to_int *)
+theory bitvec.BitVector64
+  syntax type t "(_ BitVec 64)"
+
+  syntax function zero "#x00000000"
+  syntax function ones "#xFFFFFFFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 64)"
+  syntax function to_int "(bv2int %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+end
+
+theory bitvec.BitVector32
+  syntax type t "(_ BitVec 32)"
+
+  syntax function zero "#x00000000"
+  syntax function ones "#xFFFFFFFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 32)"
+  syntax function to_int "(bv2int %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+end
+
+theory bitvec.BitVector16
+  syntax type t "(_ BitVec 16)"
+
+  syntax function zero "#x0000"
+  syntax function ones "#xFFFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 16)"
+  syntax function to_int "(bv2int %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+end
+
+theory bitvec.BitVector8
+  syntax type t "(_ BitVec 8)"
+
+  syntax function zero "#x00"
+  syntax function ones "#xFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 8)"
+  syntax function to_int "(bv2int %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high