Loading columnRed.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 4), simplifying (4), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\exists int v0; 2 * v0 + x = 0

Loading cryptarithm.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 303), simplifying (344), interpolating ...

No countermodel exists, formula is valid

Interpolants:
!(D = O) & !(N = O) & !(U = O)

Loading eqProof2.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 15), simplifying (15), interpolating ...

No countermodel exists, formula is valid

Interpolants:
c + b = 26

Loading eqProof3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 6), simplifying (6), interpolating ...

No countermodel exists, formula is valid

Interpolants:
c + b = 26

Loading eqProof4.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 5), simplifying (5), interpolating ...

No countermodel exists, formula is valid

Interpolants:
!(y = 2*d)

Loading eqProof5.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 5), simplifying (5), interpolating ...

No countermodel exists, formula is valid

Interpolants:
!(y = 2*d)

Loading eqProof6.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 6), simplifying (6), interpolating ...

No countermodel exists, formula is valid

Interpolants:
!(c + b - a = 0)

Loading eqProof.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 15), simplifying (15), interpolating ...

No countermodel exists, formula is valid

Interpolants:
a = 26

Loading surprising.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 8), simplifying (8), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\exists int v0; 5 * v0 + y = -1 | \exists int v0; 5 * v0 + y = 0

Loading inEqProof0.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 7), simplifying (7), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x >= 5

Loading inEqProof1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 2), simplifying (2), interpolating ...

No countermodel exists, formula is valid

Interpolants:
y = x

Loading inEqProof2.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 12), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
y - x = -3 | y - x = -2 | y - x = -1 | y = x

Loading inEqProof3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 2), simplifying (2), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x1 >= 1

Loading inEqProof.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 5), simplifying (5), interpolating ...

No countermodel exists, formula is valid

Interpolants:
3 * b >= a

Loading int_incompleteness2.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 8), simplifying (8), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x1 + x2 >= 5 | (x1 + x2 = 4 & \exists int v0; 6 * v0 - x2 = -1) | (x1 + x2 = 4 & \exists int v0; 6 * v0 + x2 = 2) | (-1 * x1 - x2 >= -3 & x1 + x2 >= 2 & \exists int v0; 6 * v0 - x2 = -1) | (-1 * x1 - x2 >= -2 & x1 + x2 >= 1 & \exists int v0; 6 * v0 = x2) | (x1 + x2 >= 3 & \exists int v0; 6 * v0 - x1 = -1) | (x1 + x2 >= 3 & \exists int v0; 6 * v0 = x2)

Loading int_incompleteness3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 3), simplifying (3), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\exists int v0; 6 * v0 + x1 = 8

Loading pidgeon.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 100), simplifying (161), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x3 = x1 | x2 = x1

Loading pidgeonSimplified.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 24), simplifying (39), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x3 = x1 | x2 = x1

Loading pidgeonSuperSimplified.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 3), simplifying (3), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x2 = x1

Loading prog.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 8), simplifying (8), interpolating ...

No countermodel exists, formula is valid

Interpolants:
a >= 3 | (a >= 0 & \exists int v0; 2 * v0 = a)
3 * b >= a
c - a >= 1

Loading prop0.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 6), simplifying (6), interpolating ...

No countermodel exists, formula is valid

Interpolants:
!p | q

Loading prop1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 17), simplifying (19), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\exists int v0; 2 * v0 = a & (2 * c + a - 6*b >= 2 | !p)

Loading prop2.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 4), simplifying (4), interpolating ...

No countermodel exists, formula is valid

Interpolants:
p(14, 2 * x)

Loading prop3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 4), simplifying (4), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x = 13

Loading prop4.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 7), simplifying (7), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\forall int v0; (!(2 * v0 = y) | p(v0))

Loading prop5.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 17), simplifying (18), interpolating ...

No countermodel exists, formula is valid

Interpolants:
p(2) | p(1)
p(3) | p(2) | p(1) | p(0)

Loading queen2-1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 12), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x1 - x0 = 1 | x1 - x0 = -1 | x1 = x0 | x0 - x2 >= 2

Loading queen3-1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 12), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x1 - x0 = 1 | x1 - x0 = -1 | x1 = x0 | x0 - x2 >= 2

Loading super_queen2-1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 12), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x1 - x0 = 1 | x1 - x0 = -1 | x0 - x2 >= 2

Loading super_queen3-1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 16), simplifying (17), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x2 - x1 = 2 | x2 - x1 = -2 | x2 - x1 = 1 | x2 - x1 = -1

Loading cav-ex4b.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 106), simplifying (99), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\forall int v0; \forall int v1; (h'(f(v1)) + -1 * h'(f(v0)) >= 0 | -1 >= v0 | v1 - n >= 1 | v0 - v1 >= 1 | -1 >= v1)
\exists int v0; \exists int v1; (-1 * h'(v1) + h'(v0) >= 1 & \exists int v2; (v2 >= 0 & f(v2) = v0 & \exists int v3; (n >= v3 & v3 >= v2 & v3 >= 0 & f(v3) = v1)))

Loading quan.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 7), simplifying (7), interpolating ...

No countermodel exists, formula is valid

Interpolants:
c >= 0

Loading ring_2exp10_3vars_2ite_unsat.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 2537), simplifying (2804), interpolating ...

No countermodel exists, formula is valid

Interpolants:
v2 >= 1024 | (v_princess_0 - 2*v2 = -1024 & v2 >= 512) | (v_princess_0 = 2*v2 & 511 >= v2)

Loading arrays0.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 10), simplifying (10), interpolating ...

No countermodel exists, formula is valid

Interpolants:
true
b1'1 = 0
!(prob_index'2 = 1) | !(select(prres0'1, 1) = 1)
!(prob_index'2 = 1) | !(select(prres0'1, 1) = 1)
!(prob_index'2 = 1) | !(select(prres0'1, 1) = 1)
!(prob_index'2 = 1)
!(prob_index'2 = 1)
!(prob_index'2 = 1)
!(prob_index'2 = 1)

Loading constOrderBug.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 129), simplifying (140), interpolating ...

No countermodel exists, formula is valid

Interpolants:
sym2 = 0 | (sym2 = sym1 & (sym1 = 2 | sym1 = 1))

Loading strange_concurrency.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
id1 = 0 & id0 = 2 & write1' = 33 & write0' = 16 & write1 = 33 & write0 = 32 & read1' = 33 & read0' = 16 & read1 = 33 & read0 = 32 & A4 = 0 & A3 = 1 & A2 = 2 & A1 = 3 & A0 = 4 & j2' = 0 & j1' = 33 & j0' = 16 & j2 = 2 & j1 = 1 & j0 = 0 & i2' = 0 & i1' = 0 & i0' = 0 & i2 = 32 & i1 = 32 & i0 = 32 & select(4, 33) = 0 & select(4, 32) = 0 & select(4, 16) = 0 & select(3, 33) = 0 & select(3, 16) = 0 & select(2, 33) = 1 & select(2, 16) = 0 & select(1, 33) = 1 & store(4, 32, 1) = 3 & store(3, 33, 1) = 2 & store(2, 16, 1) = 1 & store(1, 33, 2) = 0 & T(32, 32, 1, 2, 3, 2, 33, 33) & T(32, 32, 0, 1, 4, 3, 32, 32) & T(0, 0, 33, 0, 1, 0, 33, 33) & T(0, 0, 16, 33, 2, 1, 16, 16) & !(select(3, 32) = 0) & !(select(2, 33) = 0) & !(store(4, 32, 1) = 4) & !(store(3, 33, 1) = 4) & !(store(3, 33, 1) = 3) & !(store(2, 33, 1) = 1) & !(store(2, 16, 1) = 4) & !(store(2, 16, 1) = 3) & !(store(2, 16, 1) = 2) & !(store(1, 33, 2) = 4) & !(store(1, 33, 2) = 3) & !(store(1, 33, 2) = 2) & !(store(1, 33, 2) = 1)

Loading wrongInterpolant3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 141), simplifying (137), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\exists int v0; 4 * v0 + j2 + i1 = 2 & \exists int v0; 4 * v0 + j1 + i1 = 1 & \exists int v0; 4 * v0 + i1 = 0

Loading omegaBug.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
sym9 = 0 & sym8 = 0 & sym7 = 0 & sym6 = 0 & sym5 = 1 & sym4 = 2 & sym3 = 1 & sym2 = 1 & sym1 = 1 & sym0 = 268435456 & select(0, 1) = 12 & store(1, 1, 12) = 0 & store(0, 2, 3) = 0 & inUnsigned(32, 2) & inUnsigned(32, 1) & inUnsigned(32, 0) & inSigned(32, 268435456) & inArray(1) & inArray(0) & !(select(1, 1) = 12)

Loading splitEq.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 372), simplifying (277), interpolating ...

No countermodel exists, formula is valid

Interpolants:
10000000 >= x & x >= -1000000

Loading incorrectPredInterpolant.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 9), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
e - d >= 2 | (e - d = 1 & p(-1 * d)) | (e = 0 & (-1 >= d | (d = 0 & p(0))))

Loading certificateBug.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 1), simplifying (1), interpolating ...

No countermodel exists, formula is valid

Interpolants:
true

Loading missingOmegaSupport.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 1127), simplifying (994), interpolating ...

No countermodel exists, formula is valid

Interpolants:
3 * x7 + x8 + 5 * x0 + 7 * x6 + 2 * x3 >= 7 & x5 + x8 + x3 - x6 - x2 >= -1 & x5 + x2 + 2 * x0 + 4 * x6 + x3 - x8 - 2*x9 >= 5

Loading bignum_lia1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 58), simplifying (44), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x4 >= 19670160000*x1 | x4 >= 16039976000*x1 | x4 >= 9835080000*x1 | x4 >= 8019988000*x1 | x4 >= 1

Loading linear-combination-bug.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 13), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\exists int v0; 8 * v0 - x1 = -8 | \exists int v0; 8 * v0 - x1 = -7 | \exists int v0; 8 * v0 - x1 = -6 | \exists int v0; 8 * v0 - x1 = -5 | \exists int v0; 8 * v0 - x1 = -4

Loading div-right-bug.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 14), simplifying (14), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\exists int v0; 10 * v0 + c = 2

Loading tree.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 121), simplifying (100), interpolating ...

No countermodel exists, formula is valid

Interpolants:
value(c) >= 42 & -1 * value(right(left(a))) + value(right(a)) >= 34

Loading prp-2-17.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 3998), simplifying (3547), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(v_princess_0 = 402 & !(i844 = 1)) | (v_princess_0 = 30 & !(i844 = 1)) | (v_princess_0 = 19 & !(i844 = 1)) | (!(v_princess_0 = 22) & !(i844 = 1))

Loading prp-3-18.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 4170), simplifying (3669), interpolating ...

No countermodel exists, formula is valid

Interpolants:
!(v_princess_0 = 22) & !(i844 = 1)

Loading surprising25.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 8), interpolating ...

No countermodel exists, formula is valid

Interpolants:
\exists int v0; (23 >= v0 & v0 >= 0 & \exists int v1; 25 * v1 + v0 - y = 10 & \exists int v1; (-1 * v1 - v0 >= -10 & 19 >= v1 & v1 >= 0 & \exists int v2; 25 * v2 + v1 + y = 0))

Loading bignum_lia1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 58), interpolating ...

No countermodel exists, formula is valid

Interpolants:
x4 - 19670160000*x1 >= 7999 | x4 - 16039976000*x1 >= 7999 | x4 - 9835080000*x1 >= 3999 | x4 - 8019988000*x1 >= 3999 | x4 >= 7999 | \exists int v0; (x4 - 19670160000*x1 >= v0 & 7998 >= v0 & v0 >= 0 & \exists int v1; 8000 * v1 + v0 - x4 = 0) | \exists int v0; (x4 - 16039976000*x1 >= v0 & 7998 >= v0 & v0 >= 0 & \exists int v1; 8000 * v1 + v0 - x4 = 0) | \exists int v0; (x4 - 9835080000*x1 >= v0 & 3998 >= v0 & v0 >= 0 & \exists int v1; 4000 * v1 + v0 - x4 = 0) | \exists int v0; (x4 - 8019988000*x1 >= v0 & 3998 >= v0 & v0 >= 0 & \exists int v1; 4000 * v1 + v0 - x4 = 0) | \exists int v0; (x4 - v0 >= 10487999 & 10471999 >= v0 & v0 >= 0 & \exists int v1; 10480000 * v1 + v0 - x4 = -7999) | \exists int v0; (x4 - v0 >= 4000 & 3998 >= v0 & v0 >= 0 & \exists int v1; 4000 * v1 + v0 - x4 = 0) | \exists int v0; (7998 >= v0 & v0 >= 0 & \exists int v1; 8000 * v1 + v0 - x4 = 0 & x4 - v0 >= 20952000) | \exists int v0; (7998 >= v0 & v0 >= 0 & \exists int v1; 8000 * v1 + v0 - x4 = 0 & \exists int v1; (x4 - v0 - v1 >= 10480000 & 10471999 >= v1 & v1 >= 0 & \exists int v2; 10480000 * v2 + v1 + v0 - x4 = 0))

Loading ring_2exp10_3vars_0ite_unsat.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 1034), simplifying (1344)


No countermodel exists, formula is valid

Constraint: true
