Loading bignum_quant.smt2 ...
Checking satisfiability ...
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.|)
Preprocessing ...
Proving ...

unsat

Loading int_incompleteness1.smt2 ...
Checking satisfiability ...
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.|)
Preprocessing ...
Constructing countermodel ...

unsat

Loading int_incompleteness2.smt2 ...
Checking satisfiability ...
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.|)
Preprocessing ...
Constructing countermodel ...

unsat

Loading int_incompleteness3.smt2 ...
Checking satisfiability ...
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.|)
Preprocessing ...
Constructing countermodel ...

unsat

Loading init-1.smt2 ...
Checking satisfiability ...
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)
Preprocessing ...
Constructing countermodel ...

unsat

Loading MULTIPLIER_2.msat.smt2 ...
Checking satisfiability ...
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)
Preprocessing ...
Constructing countermodel ...

unsat

Loading ite.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Proving ...

unsat

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

unsat

Loading ite3.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Proving ...

unsat

Loading for_in_term.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Proving ...

unsat

Loading for_in_term2.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Constructing countermodel ...

unsat

Loading let.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Proving ...

unsat

Loading let2.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Proving ...

unsat

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

unsat

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

unsat

Loading arrays2.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Warning: adding array axioms for arity 2
Warning: treating sort (Array Int Int Int) as Int
Preprocessing ...
Proving ...

unsat

Loading arrays3.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Warning: adding array axioms
Preprocessing ...
Proving ...

unsat

Loading patternBug.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Proving ...

unsat

Loading correct-eq.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Constructing countermodel ...

unsat

Loading array-interpolation.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Warning: adding array axioms
Warning: treating sort (Array Int Int) as Int
Warning: treating sort (Array Int Int) as Int
Preprocessing ...
Constructing countermodel ...
Found proof (size 8), simplifying (8), interpolating ...

unsat

Interpolating ...
(= 0 (+ (- 42) (select b 1 ) ) ) 

Loading define-fun.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Constructing countermodel ...

unsat

Loading define-fun2.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Proving ...

unsat

Loading define-fun3.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Constructing countermodel ...

unsat

Loading define-fun-interpolation.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Constructing countermodel ...
Found proof (size 2), simplifying (2), interpolating ...

unsat

Interpolating ...
(<= 0 (+ (- 1) (+ d c ) ) ) 

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

unsat

Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Proving ...

unsat

Loading seconds.smt2 ...
Checking satisfiability ...
Preprocessing ...
Proving ...

unknown

Loading quotes.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Constructing countermodel ...

unsat

Loading extensions.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Warning: accepting command declare-const, which is not SMT-LIB 2
Warning: interpreting "~" as unary minus, like in SMT-LIB 1
Preprocessing ...
Constructing countermodel ...

unsat

Loading boolean-quant.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Warning: accepting command declare-const, which is not SMT-LIB 2
Preprocessing ...
Proving ...

unsat

Loading simple-joogie.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Constructing countermodel ...

sat

Model:
(and (and (and (and (and (and (= 0 Dnull__0 ) (= 0 Dparam_0__0 ) ) (= 0 r18290__0 ) ) (= 0 (+ (- 1) __this__0 ) ) ) (= 0 (+ (- 1) r08289__0 ) ) ) (= 0 (+ 1 DarrSizeIdx__0 ) ) ) (and Block3538_bwd Block3538_fwd ) ) 

(Block3538_bwd true)
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Preprocessing ...
Constructing countermodel ...

unsat

Loading changing_truth_value_unsafe_garbage.c.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-info :origin "SLAyer refinement benchmarks created by Jael Kriener")
Warning: ignoring (set-logic HORN)
Preprocessing ...
Proving ...

unknown

