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 & y = -2147483662 & x = -2147483660 & addSigned(32, -2147483662, 13) = 2147483647

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


No countermodel exists, formula is valid

Constraint: true
Loading ricart-agrawala7.smt2 ...
Checking satisfiability ...
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)
Preprocessing ...
Constructing countermodel ...

sat

Model:
(and (and (and (= 0 (+ (- 1) time ) ) (= 0 q ) ) (= 0 (+ (- 1) p ) ) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= 0 (+ (- 1) (s2 1 ) ) ) (= 0 (+ (- 1) (s3 1 ) ) ) ) (= 0 (+ (- 1) (ro 1 0 ) ) ) ) (= 0 (+ (- 1) (rd 0 1 ) ) ) ) (= 0 (s4 1 ) ) ) (= 0 (sn 1 ) ) ) (= 0 (+ 1 (sn 0 ) ) ) ) (= 0 (+ (- 1) (s6 1 ) ) ) ) (= 0 (s6 0 ) ) ) (= 0 (rcs2 1 ) ) ) (= 0 (rcs2 0 ) ) ) (= 0 (+ (- 1) (x 1 0 ) ) ) ) (= 0 (+ (- 1) (x 0 1 ) ) ) ) (= 0 (+ (- 1) (s0 1 ) ) ) ) (= 0 (+ (- 1) (s5 1 ) ) ) ) ) 

Loading proofBug.pri ...
Preprocessing ...
Constructing countermodel ...

Cancelled or timeout

Loading multiplication3.pri ...
Warning: introducing partial function "nonLinMult" to encode multiplication
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading vstte-problem-2-vc.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading soldiers.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting most-general constraint:
10 >= MinNum

Concrete witness:
MinNum = 10

