A poorly successful attempt to check consistency of bv theory with SMTLIB,...

A poorly successful attempt to check consistency of bv theory with SMTLIB, using a kind of "SMT realization"

drivers/cvc4-realize.drv

+(** Why3 driver specific for checking BV theory consistency with CVC4  *)
+
+prelude "(set-logic AUFBVDTNIRA)"
+(*
+    A  : Array
+    UF : Uninterpreted Function
+    BV : BitVectors
+    DT : Datatypes
+    NIRA : NonLinear Integer Reals Arithmetic
+*)
+(* prelude "(set-logic ALL_SUPPORTED)"
+   does not seem to include DT
+*)
+
+import "smt-libv2.drv"
+import "smt-libv2-bv-realization.gen"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "detect_polymorphism"
+transformation "eliminate_definition"
+(* We could keep more definitions by using
+   transformation "eliminate_definition_if_poly"
+   instead, but some proofs are lost
+   (examples/logic/triangle_inequality.why)
+*)
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_if_poly"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate_if_poly"
+transformation "encoding_smt_if_poly"
+
+(** Error messages specific to CVC4 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
+(**
+Unfortunately, there is no specific output message when CVC4 reaches its resource limit
+steplimitexceeded "??"
+*)
+
+(** Extra theories supported by CVC4 *)
+
+(* Disabled:
+   CVC4 seems less efficient with its built-in implementation than
+   with the axiomatic version
+*)
+(*
+theory int.EuclideanDivision
+   syntax function div "(div %1 %2)"
+   syntax function mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+*)
+
+import "cvc4_bv.gen"

drivers/smt-libv2-bv-realization.gen

+(* Why3 driver checking compatibility of BV theories with SMT-LIB2 *)
+
+theory bv.BV_Gen
+  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_bv "(bvlshr %1 %2)"
+  syntax function lsl_bv "(bvshl %1 %2)"
+  syntax function asr_bv "(bvashr %1 %2)"
+  syntax predicate eq "(= %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)"
+  syntax predicate slt "(bvslt %1 %2)"
+  syntax predicate sle "(bvsle %1 %2)"
+  syntax predicate sgt "(bvsgt %1 %2)"
+  syntax predicate sge "(bvsge %1 %2)"
+
+  (** Removing the axioms that should be proved instead
+    the one that are commented out are instead kept
+  *)
+
+  remove prop size_pos
+  remove prop nth_out_of_bound
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_and
+  remove prop Nth_bw_or
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop lsr_zero
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop asr_zero
+  remove prop Lsl_nth_high
+  remove prop Lsl_nth_low
+  remove prop lsl_zero
+  remove prop Nth_rotate_right
+  remove prop Nth_rotate_left
+
+(* Conversions from/to integers *)
+
+  remove prop two_power_size_val
+  remove prop max_int_val
+
+  remove prop to_uint_extensionality
+  remove prop to_int_extensionality
+
+  remove prop to_uint_bounds
+  remove prop to_uint_of_int
+
+  remove prop Of_int_zero
+  remove prop Of_int_ones
+
+  (** Arithmetic operators *)
+
+  remove prop to_uint_add
+  remove prop to_uint_add_bounded
+
+  remove prop to_uint_sub
+  remove prop to_uint_sub_bounded
+
+  remove prop to_uint_neg
+
+  remove prop to_uint_mul
+  remove prop to_uint_mul_bounded
+
+  remove prop to_uint_udiv
+  remove prop to_uint_urem
+
+  (* kept: Nth_bv_is_nth *)
+  (* kept: Nth_bv_is_nth2 *)
+  (* kept: lsr_bv_is_lsr *)
+
+  remove prop to_uint_lsr
+
+  (* kept: asr_bv_is_asr *)
+  (* kept: lsl_bv_is_lsl *)
+
+  remove prop to_uint_lsl
+
+  (* kept: rotate_left_bv_is_rotate_left *)
+  (* kept: rotate_right_bv_is_rotate_right *)
+
+  remove prop eq_sub_equiv
+  remove prop Extensionality
+
+
+end
+
+
+theory bv.BV64
+  syntax type t "(_ BitVec 64)"
+
+  syntax function zero "#x0000000000000000"
+  syntax function ones "#xFFFFFFFFFFFFFFFF"
+
+  syntax function nth_bv
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
+(* possible alternative definition :
+    "(= ((_ extract 0 0) (bvlshr %1 %2)) (_ bv1 1))"
+*)
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+end
+
+theory bv.BV32
+  syntax type t "(_ BitVec 32)"
+
+  syntax function zero "#x00000000"
+  syntax function ones "#xFFFFFFFF"
+
+  syntax function nth_bv
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+end
+
+theory bv.BV16
+  syntax type t "(_ BitVec 16)"
+
+  syntax function zero "#x0000"
+  syntax function ones "#xFFFF"
+
+  syntax function nth_bv
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+end
+
+theory bv.BV8
+  syntax type t "(_ BitVec 8)"
+
+  syntax function zero "#x00"
+  syntax function ones "#xFF"
+
+  syntax function nth_bv
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 8)) (_ bv0 8)))"
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
+end
+
+theory bv.BVConverter_Gen
+   remove allprops
+end
+
+theory bv.BVConverter_32_64
+  syntax function toBig "((_ zero_extend 32) %1)"
+  syntax function toSmall "((_ extract 31 0) %1)"
+end
+
+theory bv.BVConverter_16_64
+  syntax function toBig "((_ zero_extend 48) %1)"
+  syntax function toSmall "((_ extract 15 0) %1)"
+end
+
+theory bv.BVConverter_8_64
+  syntax function toBig "((_ zero_extend 56) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
+end
+
+theory bv.BVConverter_16_32
+  syntax function toBig "((_ zero_extend 16) %1)"
+  syntax function toSmall "((_ extract 15 0) %1)"
+end
+
+theory bv.BVConverter_8_32
+  syntax function toBig "((_ zero_extend 24) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
+end
+
+theory bv.BVConverter_8_16
+  syntax function toBig "((_ zero_extend 8) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
+end
+
+theory bv.Pow2int
+  remove allprops
+end

drivers/z3-realize.drv

+(** Why3 driver for Z3 >= 4.3.2 *)
+
+(* Do not set any logic, let z3 choose by itself
+   prelude "(set-logic AUFNIRA)"
+*)
+
+(* Counterexamples: set model parser *)
+model_parser "smtv2"
+
+
+import "smt-libv2.drv"
+import "smt-libv2-bv-realization.gen"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "detect_polymorphism"
+transformation "eliminate_definition"
+(* We could keep more definitions by using
+   transformation "eliminate_definition_if_poly"
+   instead, but some proofs are lost
+   (examples/logic/triangle_inequality.why)
+*)
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_if_poly"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+(* Prepare for counter-example query: get rid of some quantifiers (makes it
+possible to query model values of the variables in premises) and introduce
+counter-example projections  *)
+transformation "prepare_for_counterexmp"
+
+transformation "discriminate_if_poly"
+transformation "encoding_smt_if_poly"
+
+
+(** Error messages specific to Z3 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+
+(** Extra theories supported by Z3 *)
+
+(* div/mod of Z3 seems to be Euclidean Division *)
+theory int.EuclideanDivision
+   syntax function div "(div %1 %2)"
+   syntax function mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+
+theory real.FromInt
+  syntax function from_int "(to_real %1)"
+  remove prop Zero
+  remove prop One
+  remove prop Add
+  remove prop Sub
+  remove prop Mul
+  remove prop Neg
+end
+
+(* does not work: Z3 segfaults
+theory real.Trigonometry
+
+  syntax function cos "(cos %1)"
+  syntax function sin "(sin %1)"
+  syntax function pi "pi"
+  syntax function tan "(tan %1)"
+  syntax function atan "(atan %1)"
+
+end
+*)
+
+
+(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
+   have the same name for the function to_uint *)
+theory bv.BV64
+  syntax converter of_int "((_ int2bv 64) %1)"
+  syntax function to_uint "(bv2int %1)"
+end
+
+theory bv.BV32
+  syntax converter of_int "((_ int2bv 32) %1)"
+  syntax function to_uint "(bv2int %1)"
+end
+
+theory bv.BV16
+  syntax converter of_int "((_ int2bv 16) %1)"
+  syntax function to_uint "(bv2int %1)"
+end
+
+theory bv.BV8
+  syntax converter of_int "((_ int2bv 8) %1)"
+  syntax function to_uint "(bv2int %1)"
+end

examples/tests/bv-smtlib-realization.why

+
+(*
+
+run this test with:
+
+why3 ide -C ../../why3-smt-realize.conf -P cvc4r bv-smtlib-realization.why
+
+*)
+
+theory BV_Check
+
+  use import int.Int
+  use import bv.BV8
+
+  goal size_pos : size > 0
+
+(* Conversions from/to integers *)
+
+  use import bv.Pow2int
+
+  lemma two_power_size_val : two_power_size = pow2 size
+  lemma max_int_val : max_int = two_power_size - 1
+
+  lemma to_uint_extensionality :
+    forall v,v':t. to_uint v = to_uint v' -> v = v'
+
+  lemma to_int_extensionality:
+    forall v,v':t. to_int v = to_int v' -> v = v'
+
+  lemma to_uint_bounds : forall v:t. 0 <= to_uint v < two_power_size
+
+  lemma to_uint_of_int :
+    forall i. 0 <= i < two_power_size -> to_uint (of_int i) = i
+
+  lemma Of_int_zero: zero = of_int 0
+
+  lemma Of_int_ones: ones = of_int max_int
+
+  goal nth_out_of_bound:
+    forall x n. size <= n <= max_int -> nth x n = False
+
+  goal Nth_zero: forall n:int. 0 <= n < size -> nth zero n = False
+
+  goal Nth_ones:
+    (forall n. ult n size_bv -> nth_bv ones n = True) &&
+    forall n. 0 <= n < size -> ult (of_int n) size_bv && nth ones n = True
+
+  (** Bitwise operators *)
+
+  goal Nth_bw_and:
+    forall v1 v2:t, n:int. 0 <= n < size ->
+      nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n)
+
+  goal Nth_bw_or:
+    forall v1 v2:t, n:int. 0 <= n < size ->
+      nth (bw_or v1 v2) n = orb (nth v1 n) (nth v2 n)
+
+  goal Nth_bw_xor:
+    forall v1 v2:t, n:int. 0 <= n < size ->
+      nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)
+
+  goal Nth_bw_not:
+    forall v:t, n:int. 0 <= n < size ->
+      nth (bw_not v) n = notb (nth v n)
+
+  goal Lsr_nth_low:
+    forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s < size ->
+      nth (lsr b s) n = nth b (n+s)
+
+  goal Lsr_nth_high:
+    forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s >= size ->
+      nth (lsr b s) n = False
+
+  goal lsr_zero: forall x. lsr x 0 = x
+
+  goal Asr_nth_low:
+    forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s < size ->
+      nth (asr b s) n = nth b (n+s)
+
+  goal Asr_nth_high:
+    forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s >= size ->
+      nth (asr b s) n = nth b (size-1)
+
+  goal asr_zero: forall x. asr x 0 = x
+
+  goal Lsl_nth_high:
+    forall b:t,n s:int. 0 <= s <= n < size ->
+      nth (lsl b s) n = nth b (n-s)
+
+  goal Lsl_nth_low:
+    forall b:t,n s:int. 0 <= n < s ->
+      nth (lsl b s) n = False
+
+  goal lsl_zero: forall x. lsl x 0 = x
+
+  use import int.EuclideanDivision
+
+  goal Nth_rotate_right :
+    forall v n i. 0 <= i < size -> 0 <= n ->
+      nth (rotate_right v n) i = nth v (mod (i + n) size)
+
+  goal Nth_rotate_left :
+    forall v n i. 0 <= i < size -> 0 <= n ->
+      nth (rotate_left v n) i = nth v (mod (i - n) size)
+
+
+  (* comparison operators *)
+
+  goal ult_spec: forall x y. ult x y <-> Int.(<) (to_uint x) (to_uint y)
+
+  goal ule_spec: forall x y. ule x y <-> Int.(<=) (to_uint x) (to_uint y)
+
+  goal ugt_spec: forall x y. ugt x y <-> Int.(>) (to_uint x) (to_uint y)
+
+  goal uge_spec: forall x y. uge x y <-> Int.(>=) (to_uint x) (to_uint y)
+
+  goal slt_spec: forall x y. slt x y  <-> Int.(<) (to_int x) (to_int y)
+
+  goal sle_spec: forall x y. sle x y <-> Int.(<=) (to_int x) (to_int y)
+
+  goal sgt_spec: forall x y. sgt x y <-> Int.(>) (to_int x) (to_int y)
+
+  goal sge_spec: forall x y. sge x y <-> Int.(>=) (to_int x) (to_int y)
+
+  (** Arithmetic operators *)
+
+  goal to_uint_add:
+    forall v1 v2. to_uint (add v1 v2) =  mod (Int.(+) (to_uint v1) (to_uint v2)) two_power_size
+  goal to_uint_add_bounded:
+    forall v1 v2.
+      to_uint v1 + to_uint v2 < two_power_size ->
+      to_uint (add v1 v2) = to_uint v1 + to_uint v2
+
+  goal to_uint_sub:
+    forall v1 v2. to_uint (sub v1 v2) = mod (Int.(-) (to_uint v1) (to_uint v2)) two_power_size
+  goal to_uint_sub_bounded:
+    forall v1 v2.
+      0 <= to_uint v1 - to_uint v2 < two_power_size ->
+      to_uint (sub v1 v2) = to_uint v1 - to_uint v2
+
+  goal to_uint_neg:
+    forall v. to_uint (neg v) = mod (Int.(-_) (to_uint v)) two_power_size
+
+  goal to_uint_mul:
+    forall v1 v2. to_uint (mul v1 v2) = mod (Int.( * ) (to_uint v1) (to_uint v2)) two_power_size
+  goal to_uint_mul_bounded:
+    forall v1 v2.
+      to_uint v1 * to_uint v2 < two_power_size ->
+      to_uint (mul v1 v2) = to_uint v1 * to_uint v2
+
+  goal to_uint_udiv:
+    forall v1 v2. to_uint (udiv v1 v2) = div (to_uint v1) (to_uint v2)
+
+  goal to_uint_urem:
+    forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
+
+  goal to_uint_lsr:
+    forall v n : t.
+      to_uint (lsr_bv v n) = div (to_uint v) (pow2 ( to_uint n ))
+
+  goal to_uint_lsl:
+    forall v n : t.
+         to_uint (lsl_bv v n) = mod (Int.( * ) (to_uint v) (pow2 (to_uint n))) two_power_size
+
+  (* equality goals *)
+
+  goal eq_sub_equiv: forall a b i n:t.
+      eq_sub    a b (to_uint i) (to_uint n)
+  <-> eq_sub_bv a b i n
+
+  goal Extensionality: forall x y : t [eq x y]. eq x y -> x = y
+
+end
+
+theory BVConverter_Check
+
+  use import bv.BVConverter_32_64
+
+  goal toSmall_to_uint :
+    forall x. in_range x -> BV64.to_uint x = BV32.to_uint (toSmall x)
+
+  goal toBig_to_uint :
+    forall x. BV32.to_uint x = BV64.to_uint (toBig x)
+
+end

examples/tests/bv-smtlib-realization/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<prover id="0" name="CVC4 (realize)" version="1.4" timelimit="5" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
+<file name="../bv-smtlib-realization.why" expanded="true">
+<theory name="BV_Check" sum="dae3fbaa95e3691db64b6755f83ecccb" expanded="true">
+ <goal name="size_pos" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="two_power_size_val" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.02"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="max_int_val" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="to_uint_extensionality" expanded="true">
+ <proof prover="0"><result status="valid" time="2.78"/></proof>
+ </goal>
+ <goal name="to_int_extensionality" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.02"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="to_uint_bounds" expanded="true">
+ <proof prover="0"><result status="valid" time="0.06"/></proof>
+ </goal>
+ <goal name="to_uint_of_int" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.03"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="Of_int_zero" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="Of_int_ones" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="nth_out_of_bound" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="Nth_zero" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="Nth_ones" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
+  <goal name="Nth_ones.1" expl="1." expanded="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="Nth_ones.2" expl="2." expanded="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="Nth_ones.3" expl="3." expanded="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="Nth_bw_and" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="Nth_bw_or" expanded="true">
+ <proof prover="0"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="Nth_bw_xor" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="Nth_bw_not" expanded="true">
+ <proof prover="0" edited="bvmnsmtlibmnrealization-BV_Check-Nth_bw_not_1.smt2"><result status="valid" time="0.07"/></proof>
+ </goal>
+ <goal name="Lsr_nth_low" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.01"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="Lsr_nth_high" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.01"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="lsr_zero" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.01"/></proof>
+ <proof prover="1"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="Asr_nth_low" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.01"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="Asr_nth_high" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.01"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="asr_zero" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.01"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="Lsl_nth_high" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.01"/></proof>
+ <proof prover="1"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="Lsl_nth_low" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.02"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="lsl_zero" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.01"/></proof>
+ <proof prover="1"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="Nth_rotate_right" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.03"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="Nth_rotate_left" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.03"/></proof>
+ <proof prover="1"><result status="timeout" time="4.98"/></proof>
+ </goal>
+ <goal name="ult_spec" expanded="true">
+ <proof prover="0"><result status="valid" time="4.43"/></proof>
+ </goal>
+ <goal name="ule_spec" expanded="true">
+ <proof prover="0"><result status="valid" time="2.99"/></proof>
+ </goal>
+ <goal name="ugt_spec" expanded="true">
+ <proof prover="0"><result status="valid" time="4.43"/></proof>
+ </goal>
+ <goal name="uge_spec" expanded="true">
+ <proof prover="0"><result status="valid" time="3.05"/></proof>
+ </goal>
+ <goal name="slt_spec" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.03"/></proof>
+ <proof prover="1"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="sle_spec" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.03"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="sgt_spec" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.03"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="sge_spec" expanded="true">
+ <proof prover="0"><result status="unknown" time="0.02"/></proof>
+ <proof prover="1"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="to_uint_add" expanded="true">
+ <proof prover="0"><result status="timeout" time="5.01"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>
+ <goal name="to_uint_add_bounded" expanded="true">
+ <proof prover="0"><result status="timeout" time="9.99"/></proof>
+ <proof prover="1"><result status="timeout" time="4.99"/></proof>
+ </goal>