Wiki Agenda Contact Version française

Counting bits in a bit vector

Computing the number of bits in a bit vector, and various applications. This case study is detailed in Inria research report 8821.


Authors: Clément Fumex / Claude Marché

Topics: Ghost code / Bitwise operations

Tools: Why3

References: ProofInUse joint laboratory

see also the index (by topic, by tool, by reference, by year)


module BitCount8bit_fact

  use import int.Int
  use import int.NumOf
  use import bv.BV8
  use import ref.Ref

  function nth_as_bv (a i : t) : t =
    if nth_bv a i
    then (1 : t)
    else zeros

  function nth_as_int (a : t) (i : int) : int =
    if nth a i
    then 1
    else 0

  lemma nth_as_bv_is_int : forall a i.
    t'int (nth_as_bv a i) = nth_as_int a (t'int i)

    use import int.EuclideanDivision

  let ghost step1 (n x1 : t) (i : int) : unit
    requires { 0 <= i < 4 }
    requires { x1 = sub n (bw_and (lsr_bv n (1 : t)) (0x55 : t)) }
    ensures { t'int (bw_and (lsr x1 (2*i)) (0x03 : t))
            = numof (nth n) (2*i) (2*i + 2) }
    ensures { ule (bw_and (lsr x1 (2*i)) (0x03 : t)) (2 : t) }
  =
    assert { let i' = of_int i in
             let twoi = mul (2 : t) i' in
                 bw_and (lsr_bv x1 twoi) (0x03 : t)
               = add (nth_as_bv n twoi) (nth_as_bv n (add twoi (1 : t)))
             &&
                 t'int (bw_and (lsr_bv x1 twoi) (0x03 : t))
               = numof (nth n) (t'int twoi) (t'int twoi + 2) }

  let ghost step2 (n x1 x2 : t) (i : int) : unit
    requires { 0 <= i < 2 }
    requires { x1 = sub n (bw_and (lsr_bv n (1 : t)) (0x55 : t)) }
    requires { x2 = add
               (bw_and x1 (0x33 : t))
               (bw_and (lsr_bv x1 (2 : t)) (0x33 : t)) }
    ensures  { t'int (bw_and (lsr x2 (4*i)) (0x0F : t))
             = numof (nth n) (4*i) (4*i+4) }
    ensures  { ule (bw_and (lsr_bv x2 (of_int (4*i))) (0x0F : t))
                   (4 : t) }
  =
     step1 n x1 (2*i);
     step1 n x1 (2*i+1);

     assert { let i' = of_int i in
                  ult i' (2 : t)
                &&
                  of_int (4*i) = mul (4 : t) i'
                &&
                  t'int (bw_and (lsr x2 (4*i)) (0x0F : t))
                = t'int (bw_and (lsr_bv x2 (mul (4 : t) i')) (0x0F : t))
                = t'int (add (bw_and (lsr_bv x1 (mul (4 : t) i')) (0x03 : t))
                           (bw_and (lsr_bv x1 (add (mul (4 : t) i') (2 : t))) (0x03 : t)))
                = t'int (add (bw_and (lsr x1 (4*i)) (0x03 : t))
                               (bw_and (lsr x1 ((4*i)+2)) (0x03 : t)))}

  let ghost prove (n x1 x2 x3 : t) : unit
    requires { x1 = sub n (bw_and (lsr_bv n (1 : t)) (0x55 : t)) }
    requires { x2 = add
               (bw_and x1 (0x33 : t))
               (bw_and (lsr_bv x1 (2 : t)) (0x33 : t)) }
    requires { x3 = bw_and (add x2 (lsr_bv x2 (4 : t))) (0x0F : t) }
    ensures { t'int x3 = numof (nth n) 0 8 }
  =
    step2 n x1 x2 0;
    step2 n x1 x2 1;

    assert {  t'int (bw_and x2 (0x0F : t)) +
              t'int (bw_and (lsr_bv x2 (4 : t)) (0x0F : t))
            = t'int (bw_and (lsr x2 0) (0x0F : t)) +
              t'int (bw_and (lsr x2 4) (0x0F : t)) }

  let count (n : t) : t
    ensures { t'int result = numof (nth n) 0 8 }
  =
    let x = ref n in

    x := sub !x (bw_and (lsr_bv !x (1 : t)) (0x55 : t));
    let ghost x1 = !x in

    x := add
               (bw_and !x (0x33 : t))
               (bw_and (lsr_bv !x (2 : t)) (0x33 : t));
    let ghost x2 = !x in

    x := bw_and (add !x (lsr_bv !x (4 : t))) (0x0F : t);

    prove n x1 x2 !x;

    !x

end

module BitCounting32

  use import int.Int
  use import int.NumOf
  use import bv.BV32
  use import ref.Ref

  predicate step0 (n x1 : t) =
    x1 = sub n (bw_and (lsr_bv n (1 : t)) (0x55555555 : t))

  let ghost proof0 (n x1 : t) (i : int) : unit
    requires { 0 <= i < 16 }
    requires { step0 n x1 }
    ensures { t'int (bw_and (lsr x1 (2*i)) (0x03 : t))
              = numof (nth n) (2*i) (2*i + 2) }
  =
    let i' = of_int i in
    let twoi = mul (2 : t) i' in
    assert { t'int twoi = 2 * i };
    assert { t'int (add twoi (1 : t)) = t'int twoi + 1 };
    assert { t'int (bw_and (lsr_bv x1 twoi) (0x03 : t))
             = (if nth_bv n twoi then 1 else 0) +
               (if nth_bv n (add twoi (1 : t)) then 1 else 0)
             = (if nth n (t'int twoi) then 1 else 0) +
               (if nth n (t'int twoi + 1) then 1 else 0)
             = numof (nth n) (t'int twoi) (t'int twoi + 2) }

  predicate step1 (x1 x2 : t) =
    x2 = add (bw_and x1 (0x33333333 : t))
             (bw_and (lsr_bv x1 (2 : t)) (0x33333333 : t))

  let ghost proof1 (n x1 x2 : t) (i : int) : unit
    requires { 0 <= i < 8 }
    requires { step0 n x1  }
    requires { step1 x1 x2 }
    ensures  { t'int (bw_and (lsr x2 (4*i)) (0x07 : t))
               = numof (nth n) (4*i) (4*i+4) }
  =
     proof0 n x1 (2*i);
     proof0 n x1 (2*i+1);
     let i' = of_int i in
     assert { ult i' (8 : t) };
     assert { t'int (mul (4 : t) i') = 4*i };
     assert { bw_and (lsr x2 (4*i)) (0x07 : t)
              = bw_and (lsr_bv x2 (mul (4 : t) i')) (0x07 : t)
              = add (bw_and (lsr_bv x1 (mul (4 : t) i')) (0x03 : t))
                      (bw_and (lsr_bv x1 (add (mul (4 : t) i') (2 : t)))
                              (0x03 : t))
              = add (bw_and (lsr x1 (4*i)) (0x03 : t))
                      (bw_and (lsr x1 ((4*i)+2)) (0x03 : t)) }

  predicate step2 (x2:t) (x3:t) =
    x3 = bw_and (add x2 (lsr_bv x2 (4 : t))) (0x0F0F0F0F : t)

  let ghost proof2 (n x1 x2 x3 : t) (i : int) : unit
    requires { 0 <= i < 4 }
    requires { step0 n x1 }
    requires { step1 x1 x2 }
    requires { step2 x2 x3 }
    ensures  { t'int (bw_and (lsr x3 (8*i)) (0x0F : t))
             = numof (nth n) (8*i) (8*i+8) }
  =
    proof1 n x1 x2 (2*i);
    proof1 n x1 x2 (2*i+1);
    let i' = of_int i in
    assert { ult i' (4 : t) };
    assert { t'int (mul (8 : t) i') = 8*i };
    assert { t'int (add (mul (8 : t) i') (4 : t)) = 8*i+4 };
    assert { bw_and (lsr x3 (8*i)) (0x0F : t)
             = bw_and (lsr_bv x3 (mul (8 : t) i')) (0x0F : t)
             = add (bw_and (lsr_bv x2 (mul (8 : t) i')) (0x07 : t))
                   (bw_and (lsr_bv x2 (add (mul (8 : t) i') (4 : t))) (0x07 : t))
             = add (bw_and (lsr x2 (8*i)) (0x07 : t))
                   (bw_and (lsr x2 ((8*i)+4)) (0x07 : t)) }

  predicate step3 (x3:t) (x4:t) =
    x4 = add x3 (lsr_bv x3 (8 : t))

  let ghost proof3 (n x1 x2 x3 x4 : t) (i : int) : unit
    requires { 0 <= i < 2 }
    requires { step0 n x1 }
    requires { step1 x1 x2 }
    requires { step2 x2 x3 }
    requires { step3 x3 x4 }
    ensures  { t'int (bw_and (lsr x4 (16*i)) (0x1F : t))
               = numof (nth n) (16*i) (16*i+16) }
  =
    proof2 n x1 x2 x3 (2*i);
    proof2 n x1 x2 x3 (2*i+1);
    let i' = of_int i in
    assert { ult i' (2 : t) };
    assert { t'int (mul (16 : t) i') = 16*i };
    assert { t'int (add (mul (16 : t) i') (8 : t)) = 16*i+8 };
    assert { bw_and (lsr x4 (16*i)) (0x1F : t)
             = bw_and (lsr_bv x4 (mul (16 : t) i')) (0x1F : t)
             = add (bw_and (lsr_bv x3 (mul (16 : t) i')) (0x0F : t))
                   (bw_and (lsr_bv x3 (add (mul (16 : t) i') (8 : t))) (0x0F : t))
             = add (bw_and (lsr x3 (16*i)) (0x0F : t))
                   (bw_and (lsr x3 ((16*i)+8)) (0x0F : t)) }

  predicate step4 (x4:t) (x5:t) =
    x5 = add x4 (lsr_bv x4 (16 : t))

  let ghost prove (n x1 x2 x3 x4 x5 : t) : unit
    requires { step0 n x1 }
    requires { step1 x1 x2 }
    requires { step2 x2 x3 }
    requires { step3 x3 x4 }
    requires { step4 x4 x5 }
    ensures { t'int (bw_and x5 (0x3F : t)) = numof (nth n) 0 32 }
  =
    proof3 n x1 x2 x3 x4 0;
    proof3 n x1 x2 x3 x4 1;
(* moved to the stdlib
    assert { x4 = lsr x4 0 };
*)
    assert { bw_and x5 (0x3F : t)
             = add (bw_and x4 (0x1F : t)) (bw_and (lsr_bv x4 (16 : t)) (0x1F : t))
             = add (bw_and (lsr x4 0) (0x1F : t)) (bw_and (lsr x4 16) (0x1F : t)) }

  function count_logic (n:t) : int = numof (nth n) 0 32

  let count (n : t) : t
    ensures { t'int result = count_logic n }
  =
    let x = ref n in
    (* x = x - ( (x >> 1) & 0x55555555) *)
    x := sub !x (bw_and (lsr_bv !x (1 : t)) (0x55555555 : t));
    let ghost x1 = !x in
    (* x = (x & 0x33333333) + ((x >> 2) & 0x33333333) *)
    x := add (bw_and !x (0x33333333 : t))
             (bw_and (lsr_bv !x (2 : t)) (0x33333333 : t));
    let ghost x2 = !x in
    (* x = (x + (x >> 4)) & 0x0F0F0F0F *)
    x := bw_and (add !x (lsr_bv !x (4 : t))) (0x0F0F0F0F : t);
    let ghost x3 = !x in
    (* x = x + (x >> 8) *)
    x := add !x (lsr_bv !x (8 : t));
    let ghost x4 = !x in
    (* x = x + (x >> 16) *)
    x := add !x (lsr_bv !x (16 : t));

    prove n x1 x2 x3 x4 !x;

    (* return (x & 0x0000003F) *)
    bw_and !x (0x0000003F : t)

end

module Hamming
  use import int.Int
  use import int.NumOf
  use import mach.bv.BVCheck32
  use import BitCounting32
  use import HighOrd as HO

  predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i

  function hammingD_logic (a b : t) : int = NumOf.numof (nth_diff a b) 0 32

  let hammingD (a b : t) : t
    ensures { t'int result = hammingD_logic a b }
  =
    assert { forall i. 0 <= i < 32 -> nth (bw_xor a b) i <-> (nth_diff a b i) };
    count (bw_xor a b)

  lemma symmetric: forall a b. hammingD_logic a b = hammingD_logic b a

  lemma numof_ytpmE :
    forall p : int -> bool, a b : int.
    numof p a b = 0 -> (forall n : int. a <= n < b -> not p n)

  let lemma separation (a b : t)
    ensures { hammingD_logic a b = 0 <-> a = b }
  =
    assert { hammingD_logic a b = 0 -> eq_sub a b 0 32 }

  function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x

  let rec lemma numof_or (p q : int -> bool) (a b: int) : unit
    variant {b - a}
    ensures {numof (fun_or p q) a b <= numof p a b + numof q a b}
  =
    if a < b then
    numof_or p q a (b-1)

  let lemma triangleInequalityInt (a b c : t) : unit
    ensures {hammingD_logic a b + hammingD_logic b c >= hammingD_logic a c}
  =
    assert {numof (nth_diff a b) 0 32 + numof (nth_diff b c) 0 32 >=
    numof (fun_or (nth_diff a b) (nth_diff b c)) 0 32 >=
    numof (nth_diff a c) 0 32}

  lemma triangleInequality: forall a b c.
    (hammingD_logic a b) + (hammingD_logic b c) >= hammingD_logic a c

end

module AsciiCode
  use import int.Int
  use import int.NumOf
  use import number.Parity
  use import bool.Bool
  use import mach.bv.BVCheck32
  use import BitCounting32

  constant one : t = 1 : t
  constant lastbit : t = sub size_bv one

  (* let lastbit () = (sub_check size_bv one) : t *)

ASCII cheksum

In the beginning the encoding of an ascii character was done on 8 bits: the first 7 bits were used for the carracter itself while the 8th bit was used as a cheksum: a mean to detect errors. The cheksum value was the binary sum of the 7 other bits, allowing the detections of any change of an odd number of bits in the initial value. Let's prove it!


Checksum computation and correctness

A ascii character is valid if its number of bits is even. (Remember that a binary number is odd if and only if its first bit is 1)

  predicate validAscii (b : t) = even (count_logic b)

  let lemma bv_even (b:t)
    ensures { even (t'int b) <-> not (nth b 0) }
  =
    assert { not (nth_bv b zeros) <-> b = mul (2 : t) (lsr_bv b one) };
    assert { (exists k. b = mul (2 : t) k) -> not (nth_bv b zeros) };
    assert { (exists k. t'int b = 2 * k) -> (exists k. b = mul (2 : t) k) };
    assert { not (nth b 0) <-> t'int b = 2 * t'int (lsr b 1) }

  lemma bv_odd : forall b : t. odd (t'int b) <-> nth b 0

  (* use Numofbit *)

  use HighOrd as HO

  function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x

  let rec lemma numof_or (p q : int -> bool) (a b: int) : unit
    requires { forall i. a <= i < b -> not (p i) \/ not (q i) }
    variant {b - a}
    ensures {numof (fun_or p q) a b = numof p a b + numof q a b}
  =
    if a < b then
    numof_or p q a (b-1)

  let lemma count_or (b c : t)
    requires { bw_and b c = zeros }
    ensures  { count_logic (bw_or b c) = count_logic b + count_logic c }
  =
    assert { forall i. ult i size_bv ->
               not (nth_bv b i) \/ not (nth_bv c i) };
    assert { forall i. not (nth_bv b (of_int i)) \/ not (nth_bv c (of_int i))
          -> not (nth b i) \/ not (nth c i) };
    assert { numof (fun_or (nth b) (nth c)) 0 32 = numof (nth b) 0 32 + numof (nth c) 0 32 };
    assert { numof (nth (bw_or b c)) 0 32 = numof (fun_or (nth b) (nth c)) 0 32 }

The ascii checksum aim is to make any character valid in the sens that we just defined. One way to implement it is to count the number of bit of a character encoded in 7 bits, and if this number is odd, set the 8th bit to 1 if not, do nothing:

  let ascii (b : t) =
    requires { not (nth_bv b lastbit) }
    ensures  { eq_sub_bv result b zeros lastbit }
    ensures  { validAscii result }
    let c = count b in
    let maskbit = lsl_check c lastbit in
    assert { bw_and b maskbit = zeros };
    assert { even (t'int c) ->
               not (nth_bv c zeros)
            && count_logic maskbit    = 0 };
    assert { odd  (t'int c) ->
               nth_bv c zeros
            && nth maskbit 31
            && (forall i. 0 <= i < 31 -> not (nth maskbit i))
            && count_logic maskbit    = 1 };
    let code = bw_or b maskbit in
    assert { count_logic code = count_logic b + count_logic maskbit };
    code

Now, for the correctness of the checksum :

We prove that two numbers differ by an odd number of bits, i.e. are of odd hamming distance, iff one is a valid ascii character while the other is not. This imply that if there is an odd number of changes on a valid ascii character, the result will be invalid, hence the validity of the encoding.

  use Hamming

  let rec lemma tmp (a b : t) (i j : int)
      requires { i < j }
      variant { j - i }
      ensures { (even (numof (nth a) i j) /\ odd (numof (nth b) i j)) \/ (odd (numof (nth a) i j) /\ even (numof (nth b) i j))
             <-> odd (NumOf.numof (Hamming.nth_diff a b) i j) }
  =
    if i < j - 1 then
      tmp a b i (j-1)

  lemma asciiProp : forall a b.
          ((validAscii a /\ not validAscii b) \/ (validAscii b /\ not validAscii a))
      <-> odd (Hamming.hammingD_logic a b)

end


download ZIP archive

Why3 Proof Results for Project "bitcount"

Theory "bitcount.BitCount8bit_fact": fully verified in 0.29 s

ObligationsAlt-Ergo (1.01)Alt-Ergo (1.30)CVC4 (1.4)CVC4 (1.4 noBV)Z3 (4.4.1)Z3 (4.5.0)Z3 (4.5.0 noBV)
nth_as_bv_is_int---0.160.050.08---------
2. VC for step1---------------------
split_goal_wp
  1. assertion---------------------
split_goal_wp
  1. assertion------------0.020.06---
2. assertion------0.56------0.11---
2. postcondition---0.20---------0.08---
3. postcondition0.170.17---------0.08---
3. VC for step2---------------------
split_goal_wp
  1. precondition0.040.030.040.07---0.020.02
2. precondition0.020.030.040.07---0.020.02
3. precondition---------------------
split_goal_wp
  1. VC for step20.050.030.040.07---0.020.02
2. VC for step20.040.030.040.07---0.020.02
4. precondition---------------------
split_goal_wp
  1. precondition0.020.030.040.07---0.020.01
5. assertion---------------------
split_goal_wp
  1. assertion0.100.050.110.10---0.040.66
2. assertion0.100.120.16------0.04---
3. assertion0.730.84---0.12---0.07---
4. assertion------0.04------0.08---
5. assertion------2.74------0.08---
6. postcondition---3.140.050.12---0.04---
7. postcondition0.360.130.100.12---0.04---
4. VC for prove---------------------
split_goal_wp
  1. precondition0.040.030.030.04---0.020.02
2. precondition0.040.030.040.06---0.020.01
3. precondition0.040.030.040.06---0.020.02
4. precondition0.040.040.030.04---0.020.02
5. precondition0.040.040.030.06---0.020.02
6. precondition0.040.040.040.06---0.010.02
7. assertion0.120.16---0.10---0.18---
8. postcondition------0.20------0.06---
5. VC for count---------------------
split_goal_wp
  1. precondition---------------------
split_goal_wp
  1. precondition0.040.020.040.07---0.010.02
2. precondition0.050.030.040.07---0.020.02
3. precondition---------------------
split_goal_wp
  1. precondition0.050.020.040.06---0.020.02
4. postcondition0.050.030.040.05---0.020.02

Theory "bitcount.BitCounting32": fully verified in 0.00 s

ObligationsAlt-Ergo (1.01)Alt-Ergo (1.30)CVC4 (1.4)CVC4 (1.4 noBV)Z3 (4.3.2)Z3 (4.4.1)Z3 (4.5.0)Z3 (4.5.0 noBV)
1. VC for proof0------------------------
split_goal_wp
  1. assertion0.030.03------------0.04---
2. assertion0.040.04------------0.07---
3. assertion------------------------
split_goal_wp
  1. VC for proof0------------------------
introduce_premises
  1. VC for proof0------0.19---------0.12---
2. VC for proof00.410.05---0.12------------
3. VC for proof00.300.20---0.12------0.14---
4. postcondition0.160.18---0.11------0.23---
2. VC for proof1------------------------
split_goal_wp
  1. precondition0.030.030.050.06------0.020.04
2. precondition0.020.030.050.06------0.010.02
3. precondition0.040.020.050.07------0.020.03
4. precondition0.030.030.050.06------0.020.02
5. assertion0.040.04---0.10------0.060.61
6. assertion0.100.130.12---------0.04---
7. assertion------------------------
split_goal_wp
  1. VC for proof10.030.04---0.10------0.06---
2. VC for proof1------0.05---------0.12---
3. VC for proof10.040.04---1.00------0.09---
8. postcondition------0.050.13------0.06---
3. VC for proof2------------------------
split_goal_wp
  1. precondition0.040.020.050.07------0.020.03
2. precondition0.040.020.050.07------0.020.02
3. precondition0.030.030.050.07------0.020.02
4. precondition0.040.030.050.06------0.020.03
5. precondition0.030.030.050.06------0.010.01
6. precondition0.040.030.050.06------0.020.02
7. assertion0.060.05---0.11------0.060.62
8. assertion0.140.040.06---------0.04---
9. assertion0.110.020.11---------0.04---
10. assertion------------------------
split_goal_wp
  1. VC for proof20.030.04---0.10------0.09---
2. VC for proof2------0.07------0.020.11---
3. VC for proof20.030.04---0.10------0.09---
11. postcondition------0.060.14------0.10---
4. VC for proof3------------------------
split_goal_wp
  1. precondition0.040.030.050.06------0.020.03
2. precondition0.030.020.060.07------0.010.02
3. precondition0.030.030.050.06------0.020.02
4. precondition0.040.020.060.07------0.020.02
5. precondition0.030.030.060.06------0.030.03
6. precondition0.030.020.070.07------0.020.02
7. precondition0.040.030.060.06------0.020.02
8. precondition0.040.030.060.07------0.010.02
9. assertion0.050.04---0.10------0.060.65
10. assertion0.260.040.12---------0.04---
11. assertion0.030.030.14---------0.04---
12. assertion------------------------
split_goal_wp
  1. VC for proof30.040.04---0.10------0.03---
2. VC for proof3------0.07---------0.15---
3. VC for proof30.030.04---0.08------0.06---
13. postcondition------0.170.12------0.16---
5. VC for prove------------------------
split_goal_wp
  1. precondition0.040.030.040.04------0.020.02
2. precondition0.040.030.050.06------0.020.02
3. precondition0.040.030.050.06------0.020.02
4. precondition0.040.030.060.06------0.020.02
5. precondition0.040.040.050.06------0.020.02
6. precondition0.040.030.040.04------0.020.02
7. precondition0.040.030.060.06------0.020.02
8. precondition0.050.030.060.06------0.010.02
9. precondition0.040.030.050.06------0.010.02
10. precondition0.050.030.050.06------0.020.02
11. assertion------------------------
split_goal_wp
  1. VC for prove------0.04---Timeout (6s)---0.03---
2. VC for prove0.040.06---0.09---------0.23
12. postcondition------0.210.11------0.21---
6. VC for count------------------------
split_goal_wp
  1. precondition0.040.030.020.08------0.040.23
2. precondition0.030.030.030.08------0.390.62
3. precondition0.050.030.020.08------0.120.64
4. precondition0.030.030.030.08------0.080.61
5. precondition0.040.030.030.09------0.250.59
6. postcondition0.050.110.050.09------0.040.22

Theory "bitcount.Hamming": fully verified in 9.16 s

ObligationsAlt-Ergo (1.01)Alt-Ergo (1.30)CVC4 (1.4)CVC4 (1.4 noBV)Z3 (4.4.1)Z3 (4.5.0)Z3 (4.5.0 noBV)
1. VC for hammingD---------------------
split_goal_wp
  1. assertion0.832.70---0.07---------
2. postconditionTimeout (6s)1.02---------0.08---
symmetric2.290.39---------0.12---
numof_ytpmE------1.201.30---------
4. VC for separation---------------------
split_goal_wp
  1. assertion0.470.20---------0.08---
2. postcondition---------------------
split_goal_wp
  1. VC for separation0.040.05---0.08------0.22
2. VC for separation0.140.16---------0.03---
5. VC for numof_orTimeout (6s)2.810.340.39---0.06---
6. VC for triangleInequalityInt---------------------
split_goal_wp
  1. assertion---------------------
split_goal_wp
  1. VC for triangleInequalityInt0.030.020.070.090.020.040.22
2. VC for triangleInequalityInt------------0.08------
2. postcondition0.030.040.080.040.020.050.65
triangleInequality0.050.030.040.10---0.030.01

Theory "bitcount.AsciiCode": fully verified in 2.93 s

ObligationsAlt-Ergo (1.01)Alt-Ergo (1.30)CVC4 (1.4)CVC4 (1.4 noBV)Z3 (4.4.1)Z3 (4.5.0)Z3 (4.5.0 noBV)
1. VC for bv_even---------------------
split_goal_wp
  1. assertion------0.06------0.04---
2. assertion------0.04------0.04---
3. assertion1.210.43---------------
4. assertion---------------------
split_goal_wp
  1. VC for bv_even---1.50---------------
2. VC for bv_even---0.06---------------
5. postcondition0.140.14---------------
bv_odd0.050.040.030.09---0.04---
3. VC for numof_or------0.250.36---0.06---
4. VC for count_or---------------------
split_goal_wp
  1. assertion------0.09------0.05---
2. assertion0.030.04---0.10------0.23
3. assertion---------------0.04---
4. assertion---------1.81---------
5. postcondition0.060.040.080.13---0.05---
5. VC for ascii---------------------
split_goal_wp
  1. precondition---0.090.050.11---0.01---
2. assertion------0.10------0.04---
3. assertion---------------------
split_goal_wp
  1. assertion---0.08---0.10------0.25
2. assertion------0.13------------
4. assertion---------------------
split_goal_wp
  1. assertion---0.17---0.10------0.24
2. assertion---0.16---0.14---------
3. assertion---0.240.170.11---------
4. assertion---------------0.09---
5. assertion0.050.04---0.11---------
6. postcondition------0.111.55---0.04---
7. postcondition0.200.18---0.52---0.06---
6. VC for tmp---------------------
split_goal_wp
  1. variant decrease0.020.030.040.07---0.040.04
2. precondition0.020.030.020.08---0.020.01
3. postcondition---------------0.73---
4. postcondition---2.064.311.420.265.75---
asciiProp1.510.260.050.13---0.06---