Loading arrays0.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
res3 = 123 & res2 = 34 & res1 = 13

Concrete witness:
res3 = 123 & res2 = 34 & res1 = 13

Loading arrays1.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading arrays2.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading arrays0b.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
res3 = 123 & res2 = 34 & res1 = 13

Concrete witness:
res3 = 123 & res2 = 34 & res1 = 13

Loading arrays1b.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading arrays2b.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading SET027p3.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading SET063p3-clauses.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading PUZ031p1-clauses.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading functions2b.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading functions4.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading functions5.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading sepLogic0.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
X = 3

Concrete witness:
X = 3

Loading multiplication.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading multiplication2.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading group1.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading betaTaskBug.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading factNormalisationBug.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading instantiationBug.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading transitivityCounterExample.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
b = 3 & a = 0 & p(1, 2) & p(0, 2) & p(0, 1) & p(0, 0) & !p(0, 3)

Loading arrayProperties.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading eps1.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading eps2.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading eps3.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading eps4.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading matchableCheckBug.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

