Loading bignum_quant.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (set-info :source | SMT-COMP'06 organizers |)
Warning: ignoring (set-info :smt-lib-version 2.0)
Warning: ignoring (set-info :category "check")
Warning: ignoring (set-info :status unsat)
Warning: ignoring (set-info :notes |This benchmark is designed to check if the DP supports bignumbers.|)
Warning: ignoring (check-sat)
Warning: ignoring (exit)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading int_incompleteness1.smt2 ...
Warning: ignoring (set-logic QF_LIA)
Warning: ignoring (set-info :source | SMT-COMP'06 Organizers |)
Warning: ignoring (set-info :smt-lib-version 2.0)
Warning: ignoring (set-info :category "check")
Warning: ignoring (set-info :status unsat)
Warning: ignoring (set-info :notes |This benchmark is designed to check if the integer DP is complete.|)
Warning: ignoring (check-sat)
Warning: ignoring (exit)
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading int_incompleteness2.smt2 ...
Warning: ignoring (set-logic QF_LIA)
Warning: ignoring (set-info :source | Leonardo de Moura |)
Warning: ignoring (set-info :smt-lib-version 2.0)
Warning: ignoring (set-info :category "check")
Warning: ignoring (set-info :status unsat)
Warning: ignoring (set-info :notes |This benchmark is designed to check if the integer DP is complete.|)
Warning: ignoring (check-sat)
Warning: ignoring (exit)
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading int_incompleteness3.smt2 ...
Warning: ignoring (set-logic QF_LIA)
Warning: ignoring (set-info :source | Leonardo de Moura |)
Warning: ignoring (set-info :smt-lib-version 2.0)
Warning: ignoring (set-info :category "check")
Warning: ignoring (set-info :status unsat)
Warning: ignoring (set-info :notes |This benchmark is designed to check if the integer DP is complete.|)
Warning: ignoring (check-sat)
Warning: ignoring (exit)
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading init-1.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (set-info :source |
      Tokeneer case study <http://www.adacore.com/home/products/gnatpro/tokeneer/>
  |)
Warning: ignoring (set-info :smt-lib-version 2.0)
Warning: ignoring (set-info :category "industrial")
Warning: ignoring (set-info :status unknown)
Warning: ignoring (check-sat)
Warning: ignoring (exit)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading MULTIPLIER_2.msat.smt2 ...
Warning: ignoring (set-logic QF_LIA)
Warning: ignoring (set-info :source |
Mathsat benchmarks available from http://mathsat.itc.it

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
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 ...

No countermodel exists, formula is valid

Loading ite.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading ite2.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading ite3.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading for_in_term.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading for_in_term2.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading let.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading let2.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading divmod.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading arrays.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: adding array axioms
Warning: treating sort (Array Int Int) as Int
Warning: ignoring (check-sat)
Warning: ignoring (exit)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading patternBug.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Warning: ignoring (exit)
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading correct-eq.smt2 ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (check-sat)
Warning: ignoring (exit)
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

