Merge branch 'master' into claude

Conflicts:
	drivers/cvc4_bare.drv
	drivers/smt-libv2.drv
	drivers/z3_bare.drv

Makefile.in

@@ -47,7 +47,8 @@ OCAMLBEST = @OCAMLBEST@
 OCAMLVERSION = @OCAMLVERSION@
 COQC      = @COQC@
 COQDEP    = @COQDEP@
-CAMLP5O   = @CAMLP5O@
+COQCAMLP  = @COQCAMLP@
+COQCAMLPLIB = @COQCAMLPLIB@
 FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
 
 ifeq (@enable_menhirLib@,yes)
@@ -119,9 +120,9 @@ CLEANLIBS =
 GENERATED =
 
 install_local::
-	ln -s ../drivers share/drivers
-	ln -s ../modules share/modules
-	ln -s ../theories share/theories
+	ln -s -n -f ../drivers share/drivers
+	ln -s -n -f ../modules share/modules
+	ln -s -n -f ../theories share/theories
 
 ##############
 # Why3 library
@@ -769,7 +770,7 @@ COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
 COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
 
 COQPTREES = kernel interp intf lib library parsing pretyping proofs printing tactics toplevel
-COQPINCLUDES = -I src/coq-tactic -I +camlp5 $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
+COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
 
 $(COQPDEP): DEPFLAGS += -I src/coq-tactic
 $(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
@@ -796,8 +797,8 @@ lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
 	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
 
 src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
-	$(if $(QUIET),@echo 'Camlp5   $<' &&) \
-	    $(CAMLP5O) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
+	$(if $(QUIET),@echo 'Camlp    $<' &&) \
+	    $(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
 
 src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
 	$(if $(QUIET),@echo 'Coqc     $<' &&) \

configure.in

@@ -275,8 +275,6 @@ if test "$MENHIR" = no ; then
 	AC_MSG_ERROR(Cannot find menhir.)
 fi
 
-AC_CHECK_PROG(CAMLP5O,camlp5o,camlp5o,no)
-
 ## Where are the library we need
 # we look for ocamlfind; if not present, we just don't use it to find
 # libraries
@@ -496,6 +494,10 @@ else
         AC_MSG_CHECKING(Coq version)
         COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
 
+        #Even if the name of the variable is CAMLP4 the value can be camlp5
+        COQCAMLP=$(eval `coqtop -config`; echo ${CAMLP4BIN}${CAMLP4}o)
+        COQCAMLPLIB=$(eval `coqtop -config`; echo ${CAMLP4LIB})
+
         case $COQVERSION in
           8.4*)
 	        enable_coq_support=yes
@@ -730,7 +732,8 @@ AC_SUBST(MENHIR)
 AC_SUBST(enable_profiling)
 AC_SUBST(enable_bin_annot)
 
-AC_SUBST(CAMLP5O)
+AC_SUBST(COQCAMLP)
+AC_SUBST(COQCAMLPLIB)
 
 AC_SUBST(enable_ide)
 AC_SUBST(LABLGTK2LIB)

drivers/cvc4.drv

@@ -58,3 +58,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

-(* Why3 driver for SMT-LIB2 syntax, including bit-vectors *)
+(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
 
 prelude ";;; generated by SMT-LIB2 driver"
 
@@ -18,10 +18,9 @@ prelude "(set-logic AUFNIRA)"
 
 printer "smtv2"
 filename "%f-%t-%g.smt2"
-
-valid "^unsat"
 unknown "^\\(unknown\\|sat\\|Fail\\)" ""
 time "why3cpulimit time : %s s"
+valid "^unsat"
 
 
 theory BuiltIn
@@ -41,7 +40,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)"
@@ -70,7 +69,6 @@ theory int.Int
 
 end
 
-
 theory real.Real
 
   prelude ";;; SMT-LIB2: real arithmetic"
@@ -80,7 +78,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)"
@@ -153,50 +151,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"
@@ -227,6 +212,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)"
@@ -236,12 +222,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
@@ -371,7 +351,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)"
 
@@ -386,7 +365,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
@@ -412,3 +391,84 @@ theory bv.BVConverter_8_16
 
   remove prop back_from_bigBV
 end
+
+theory bitvec.Pow2int
+
+  remove prop Power_0
+  remove prop Power_s
+  remove prop Power_1
+  remove prop Power_sum
+  remove prop pow2pos
+  remove prop Div_mult_inst
+  remove prop Div_double
+  remove prop Div_pow
+  remove prop Div_double_neg
+  remove prop Div_pow2
+  remove prop Div_div_pow
+  remove prop Mod_pow2_gen
+  remove prop pow2_0
+  remove prop pow2_1
+  remove prop pow2_2
+  remove prop pow2_3
+  remove prop pow2_4
+  remove prop pow2_5
+  remove prop pow2_6
+  remove prop pow2_7
+  remove prop pow2_8
+  remove prop pow2_9
+  remove prop pow2_10
+  remove prop pow2_11
+  remove prop pow2_12
+  remove prop pow2_13
+  remove prop pow2_14
+  remove prop pow2_15
+  remove prop pow2_16
+  remove prop pow2_17
+  remove prop pow2_18
+  remove prop pow2_19
+  remove prop pow2_20
+  remove prop pow2_21
+  remove prop pow2_22
+  remove prop pow2_23
+  remove prop pow2_24
+  remove prop pow2_25
+  remove prop pow2_26
+  remove prop pow2_27
+  remove prop pow2_28
+  remove prop pow2_29
+  remove prop pow2_30
+  remove prop pow2_31
+  remove prop pow2_32
+  remove prop pow2_33
+  remove prop pow2_34
+  remove prop pow2_35
+  remove prop pow2_36
+  remove prop pow2_37
+  remove prop pow2_38
+  remove prop pow2_39
+  remove prop pow2_40
+  remove prop pow2_41
+  remove prop pow2_42
+  remove prop pow2_43
+  remove prop pow2_44
+  remove prop pow2_45
+  remove prop pow2_46
+  remove prop pow2_47
+  remove prop pow2_48
+  remove prop pow2_49
+  remove prop pow2_50
+  remove prop pow2_51
+  remove prop pow2_52
+  remove prop pow2_53
+  remove prop pow2_54
+  remove prop pow2_55
+  remove prop pow2_56
+  remove prop pow2_57
+  remove prop pow2_58
+  remove prop pow2_59
+  remove prop pow2_60
+  remove prop pow2_61
+  remove prop pow2_62
+  remove prop pow2_63
+  remove prop pow2_64
+end

drivers/z3.drv

@@ -26,6 +26,9 @@ transformation "encoding_smt"
 
 outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
 timeout "interrupted by timeout"
+(* stop reporting Z3 2.19 warnings as errors *)
+fail "^(error \"\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\)\\(.*\\)\")" "Error: \1"
+x
 
 (** Extra theories supported by Z3 *)
 
@@ -60,3 +63,266 @@ theory real.Trigonometry
 
 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 "((_ int2bv 64) %1)"
+  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
+