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

Formula is valid, resulting constraint:
true

Loading tarskiGeometry2.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading group0.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading counterExampleBug.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
(z + -2147483647 = 0 & y + 2147483662 = 0 & x + 2147483660 = 0 & addSigned(32, -2147483662, 13, 2147483647))

Loading omega_problem__031.smt.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 1), simplifying (1)


No countermodel exists, formula is valid

Constraint: true
Loading ricart-agrawala7.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (set-info :source | An Optimal Algorithm for Mutual Exclusion in Computer Networks. Glenn Ricart and Ashok K. Agrawala. Communications of the ACM Vol.: 24 Number: 1. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo  de Moura |)
Warning: ignoring (set-info :smt-lib-version 2.0)
Warning: ignoring (set-info :category "industrial")
Warning: ignoring (set-info :status unsat)
Warning: ignoring (check-sat)
Warning: ignoring (exit)
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
(time + -1 = 0 & q = 0 & p + -1 = 0 & s2(1, 1) & s3(1, 1) & ro(1, 0, 1) & rd(0, 1, 1) & s4(1, 0) & sn(1, 0) & sn(0, -1) & s6(1, 1) & s6(0, 0) & rcs2(1, 0) & rcs2(0, 0) & x(1, 0, 1) & x(0, 1, 1) & s0(1, 1) & s5(1, 1))

