## 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 int.Int
use int.NumOf
use bv.BV8
use 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 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)) }
(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)) }
(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

(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 int.Int
use int.NumOf
use bv.BV32
use 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 int.Int
use int.NumOf
use mach.bv.BVCheck32
use BitCounting32

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 : 'a -> bool) : 'a -> bool = fun 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

```

## ASCII checksum

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

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

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

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

```

#### Checksum computation and correctness

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

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

```  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 *)

function fun_or (f g : 'a -> bool) : 'a -> bool = fun 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` function makes any character valid in the sense that we just defined. One way to implement it is to count the number of 1-bits of a character encoded on 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 = u_lsl c (31:t) 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
&& (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 implies 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

```

# Why3 Proof Results for Project "bitcount"

## Theory "bitcount.BitCount8bit_fact": fully verified

 Obligations Alt-Ergo 2.0.0 CVC4 1.4 CVC4 1.4 (noBV) Z3 4.4.1 Z3 4.4.1 (noBV) nth_as_bv_is_int 0.16 0.05 0.08 --- --- VC for step1 --- --- --- --- --- split_goal_right assertion --- --- --- --- --- split_goal_right assertion --- --- --- 0.02 --- assertion --- 0.56 --- --- --- postcondition 0.20 --- --- --- --- postcondition 0.03 --- --- --- --- VC for step2 --- --- --- --- --- split_goal_right precondition 0.04 0.04 0.07 0.02 0.02 precondition 0.02 0.04 0.07 0.02 0.02 precondition --- --- --- --- --- split_goal_right VC for step2 0.05 0.04 0.07 0.02 0.02 VC for step2 0.04 0.04 0.07 0.02 0.02 precondition --- --- --- --- --- split_goal_right precondition 0.02 0.04 0.07 0.02 0.01 assertion --- --- --- --- --- split_goal_right assertion 0.10 0.11 0.10 --- 0.67 assertion 0.10 0.16 --- --- --- assertion 0.73 --- 0.12 0.07 --- assertion --- 0.04 --- --- --- assertion --- 3.31 --- --- --- postcondition 2.70 0.05 0.12 0.04 --- postcondition 0.08 0.10 0.12 0.04 --- VC for prove --- --- --- --- --- split_goal_right precondition 0.04 0.03 0.04 0.02 0.02 precondition 0.04 0.04 0.06 0.02 0.01 precondition 0.04 0.04 0.06 0.02 0.02 precondition 0.04 0.03 0.04 0.02 0.02 precondition 0.04 0.03 0.06 0.02 0.02 precondition 0.04 0.04 0.06 0.01 0.02 assertion 0.12 --- 0.10 --- --- postcondition --- 0.20 --- --- --- VC for count --- --- --- --- --- split_goal_right precondition --- --- --- --- --- split_goal_right precondition 0.05 0.04 0.06 0.02 0.02 precondition 0.05 0.04 0.07 0.02 0.02 precondition --- --- --- --- --- split_goal_right precondition 0.04 0.04 0.07 0.01 0.02 postcondition 0.05 0.04 0.05 0.02 0.02

## Theory "bitcount.BitCounting32": fully verified

 Obligations Alt-Ergo 2.0.0 CVC4 1.4 CVC4 1.4 (noBV) Z3 4.4.1 Z3 4.4.1 (noBV) VC for proof0 --- --- --- --- --- split_goal_right assertion 0.03 --- --- --- --- assertion 0.04 --- --- --- --- assertion --- --- --- --- --- split_goal_right VC for proof0 --- --- --- --- --- introduce_premises VC for proof0 --- 0.19 --- --- --- VC for proof0 0.02 --- 0.12 --- --- VC for proof0 0.16 --- 0.12 0.02 --- postcondition 0.18 --- 0.11 0.08 --- VC for proof1 --- --- --- --- --- split_goal_right precondition 0.03 0.05 0.06 0.02 0.04 precondition 0.03 0.05 0.06 0.02 0.02 precondition 0.04 0.05 0.07 0.02 0.03 precondition 0.02 0.05 0.06 0.01 0.02 assertion 0.04 --- 0.10 --- 0.61 assertion 0.05 0.12 --- --- --- assertion --- --- --- --- --- split_goal_right VC for proof1 0.03 --- 0.10 0.06 --- VC for proof1 --- 0.05 --- 0.12 --- VC for proof1 0.04 --- 1.29 --- --- postcondition --- 0.05 0.13 --- --- VC for proof2 --- --- --- --- --- split_goal_right precondition 0.04 0.05 0.07 0.02 0.03 precondition 0.03 0.05 0.06 0.01 0.01 precondition 0.04 0.05 0.06 0.02 0.02 precondition 0.04 0.05 0.06 0.02 0.03 precondition 0.04 0.05 0.07 0.02 0.02 precondition 0.03 0.05 0.07 0.02 0.02 assertion 0.06 --- 0.11 --- 0.57 assertion 0.14 0.06 --- --- --- assertion 0.11 0.11 --- --- --- assertion --- --- --- --- --- split_goal_right VC for proof2 0.03 --- 0.10 0.27 --- VC for proof2 --- 0.07 --- 0.02 --- VC for proof2 0.03 --- 0.10 0.70 --- postcondition --- 0.06 0.14 --- --- VC for proof3 --- --- --- --- --- split_goal_right precondition 0.04 0.05 0.06 0.02 0.03 precondition 0.03 0.07 0.07 0.02 0.02 precondition 0.04 0.06 0.06 0.02 0.02 precondition 0.04 0.06 0.07 0.01 0.02 precondition 0.03 0.06 0.06 0.03 0.03 precondition 0.03 0.06 0.07 0.01 0.02 precondition 0.03 0.05 0.06 0.02 0.02 precondition 0.04 0.06 0.07 0.02 0.02 assertion 0.05 --- 0.10 --- 0.49 assertion 0.09 0.12 --- --- --- assertion 0.03 0.14 --- --- --- assertion --- --- --- --- --- split_goal_right VC for proof3 0.04 --- 0.10 4.64 --- VC for proof3 --- 0.07 --- 0.02 --- VC for proof3 0.03 --- 0.08 5.18 --- postcondition --- 0.17 0.12 --- --- VC for prove --- --- --- --- --- split_goal_right precondition 0.04 0.04 0.04 0.02 0.02 precondition 0.04 0.05 0.06 0.02 0.02 precondition 0.05 0.06 0.06 0.01 0.02 precondition 0.04 0.05 0.06 0.01 0.02 precondition 0.05 0.05 0.06 0.02 0.02 precondition 0.04 0.04 0.04 0.02 0.02 precondition 0.04 0.06 0.06 0.02 0.02 precondition 0.04 0.05 0.06 0.02 0.02 precondition 0.04 0.06 0.06 0.02 0.02 precondition 0.04 0.05 0.06 0.02 0.02 assertion --- --- --- --- --- split_goal_right VC for prove --- 0.04 --- 0.03 --- VC for prove 0.04 --- 0.09 --- 0.10 postcondition --- 0.20 0.11 --- --- VC for count --- --- --- --- --- split_goal_right precondition 0.04 0.02 0.08 0.04 0.10 precondition 0.03 0.03 0.08 0.06 0.53 precondition 0.05 0.02 0.08 0.12 0.61 precondition 0.03 0.03 0.08 0.08 0.54 precondition 0.04 0.03 0.09 0.22 0.59 postcondition 0.05 0.05 0.09 0.04 0.22

## Theory "bitcount.Hamming": fully verified

 Obligations Alt-Ergo 2.0.0 Alt-Ergo 2.4.1 CVC4 1.4 CVC4 1.4 (noBV) Z3 4.4.1 Z3 4.4.1 (noBV) VC for hammingD --- --- --- --- --- --- split_goal_right assertion 4.58 --- --- 0.07 --- --- postcondition 1.12 --- --- --- 0.02 --- symmetric 0.23 --- --- --- 0.12 --- numof_ytpmE --- --- 1.32 1.62 --- --- VC for separation --- --- --- --- --- --- split_goal_right assertion --- 0.42 --- --- --- --- postcondition --- --- --- --- --- --- split_goal_right VC for separation 0.04 --- --- 0.08 --- 0.22 VC for separation 0.14 --- --- --- 0.03 --- VC for numof_or 2.98 --- 0.34 0.39 0.06 --- VC for triangleInequalityInt --- --- --- --- --- --- split_goal_right assertion --- --- --- --- --- --- split_goal_right VC for triangleInequalityInt 0.03 --- 0.07 0.09 0.02 0.09 VC for triangleInequalityInt --- --- 7.20 --- --- --- postcondition 0.03 --- 0.08 0.04 0.02 0.55 triangleInequality 0.05 --- 0.04 0.10 0.03 0.01

## Theory "bitcount.AsciiCode": fully verified

 Obligations Alt-Ergo 2.0.0 CVC4 1.4 CVC4 1.4 (noBV) CVC4 1.6 Z3 4.4.1 Z3 4.4.1 (noBV) VC for bv_even --- --- --- --- --- --- split_goal_right assertion --- 0.06 --- --- 0.04 --- assertion --- 0.04 --- --- 0.04 --- assertion 0.96 --- --- --- --- --- assertion --- --- --- --- --- --- split_goal_right VC for bv_even 0.35 --- --- --- --- --- VC for bv_even 0.06 --- --- --- --- --- postcondition 0.14 --- --- --- --- --- bv_odd 0.05 0.03 0.09 --- --- --- VC for numof_or --- 0.31 0.60 --- 0.06 --- VC for count_or --- --- --- --- --- --- split_goal_right assertion --- 0.09 --- --- 0.05 --- assertion 0.03 --- 0.10 --- --- 0.10 assertion --- --- --- --- 0.04 --- assertion --- --- 2.25 --- --- --- postcondition 0.06 0.08 0.13 --- 0.05 --- VC for ascii --- --- --- --- --- --- split_goal_right out-of-bounds shifting 0.09 0.05 0.11 --- 0.01 --- assertion --- 0.10 --- --- --- --- assertion 0.18 --- --- --- --- --- assertion --- --- --- --- --- --- split_goal_right assertion 0.02 --- 0.10 --- --- 0.11 assertion 0.04 --- 0.14 --- --- --- assertion 0.02 0.17 0.11 --- --- --- assertion --- --- --- --- 0.09 --- assertion --- --- --- 0.09 --- --- postcondition --- 0.11 2.18 --- --- --- postcondition 0.21 --- 1.09 --- 0.06 --- VC for tmp --- --- --- --- --- --- split_goal_right variant decrease 0.02 0.04 0.07 --- 0.04 0.04 precondition 0.02 0.02 0.08 --- 0.02 0.01 postcondition --- --- --- --- 0.95 --- asciiProp 0.12 0.05 0.13 --- 0.28 ---