Loading bitvectorArith3.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting most-general constraint:

Concrete witness:

Loading bitvectorArith4.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting most-general constraint:

Concrete witness:

Loading omegaBug.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting most-general constraint:

Concrete witness:

Loading splitting.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting most-general constraint:

Concrete witness:

Loading closingConstraintBug.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting most-general constraint:
(O1 = I1 & (I1 >= 8 | (!(I1 = 0) & 1 >= I1))) | (O1 = 0 & !(I1 = 1)) | (!(O1 = I1) & !(O1 = 0))

Concrete witness:
O1 = 8 & I1 = 8

