c launch: /home/mathias/runs/boolector/tacas2016/20161015-boolector-bv-synth=4/benchmarks /data/starexec/2015-06-01/BV/wintersteiger/fmsd13/ /home/mathias/runs/boolector/tacas2016/20161015-boolector-bv-synth=4 --time-limit=1200 --space-limit=7000 /home/mathias/runs/boolector/tacas2016/20161015-boolector-bv-synth=4/boolector -v --ef:synth=4
c host: atom24
c benchmark: /data/starexec/2015-06-01/BV/wintersteiger/fmsd13/fixpoint/small-seq-fixpoint-6.smt2
c solver: /home/mathias/runs/boolector/tacas2016/20161015-boolector-bv-synth=4/boolector
c solver options: -v --ef:synth=4
[btor>main] Boolector Version 2.999 4f7837876cf9c28f42649b368eaffaf03c7e1357
[btor>main] -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_PICOSAT -DBTOR_USE_LINGELING -DBTOR_USE_MINISAT
[btor>main] released Sat Oct 15 13:25:35 CEST 2016
[btor>main] compiled Sat Oct 15 13:25:35 CEST 2016
[btor>main] gcc (Ubuntu 4.8.4-2ubuntu1~14.04.3) 4.8.4
[btor>main] setting signal handlers
[btor>main] no time limit given
[btor>parse] parsing '/data/starexec/2015-06-01/BV/wintersteiger/fmsd13/fixpoint/small-seq-fixpoint-6.smt2'
[btor>smt2] parsed 6 commands in 0.00 seconds
[btor>slvef] enabled ef engine
[btor>skel] found 1 skeleton literals in 1 constraints
[btor>skel] skeleton preprocessing result 0
[btor>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[btor>core] 1 rewriting rounds in 0.0 seconds
[btor>core] simplification returned 0
[forall>slvfun] enabled core engine
[exists>slvfun] enabled core engine
[forall>slvfun] calling SAT
[forall>skel] found 0 skeleton literals in 0 constraints
[forall>skel] skeleton preprocessing result 0
[forall>skel] skeleton preprocessing produced 0 new constraints in 0.0 seconds
[forall>core] 1 rewriting rounds in 0.0 seconds
[forall>core] simplification returned 10
[forall>sat] Lingeling allows both incremental and non-incremental mode
[forall>sat] initialized Lingeling
[lingeling] Lingeling
[lingeling] 
[lingeling] Version bbc 923038088b727dcc8bd03aa8dfb5013bd03bf8c4
[lingeling] 
[lingeling] Copyright (C) 2010-2016 Armin Biere JKU Linz Austria.
[lingeling] All rights reserved.
[lingeling] 
[lingeling] released Sat May 28 15:42:42 CEST 2016
[lingeling] compiled Sat May 28 15:42:42 CEST 2016
[lingeling] 
[lingeling] gcc (Ubuntu 4.8.4-2ubuntu1~14.04) 4.8.4
[lingeling] -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
[lingeling] -DNLGLFILES -DNLGLDEMA
[lingeling] Linux cluster2 3.13.0-63-generic x86_64
[lingeling] 
[forall>slvfun] 2626 AIG vars, 26247 AIG ands, 19761 CNF vars, 55961 CNF clauses
[forall>slvfun] SAT call 1 returned 10 in 0.741 seconds
[exists>slvfun] calling SAT
[exists>core] replaced 13 embedded constraints in 0 seconds
[exists>skel] found 40 skeleton literals in 13 constraints
[exists>skel] skeleton preprocessing result 0
[exists>skel] skeleton preprocessing produced 1 new constraints in 0.0 seconds
[exists>core] 1 rewriting rounds in 0.0 seconds
[exists>core] simplification returned 0
[exists>sat] Lingeling allows both incremental and non-incremental mode
[exists>sat] initialized Lingeling
[lingeling] Lingeling
[lingeling] 
[lingeling] Version bbc 923038088b727dcc8bd03aa8dfb5013bd03bf8c4
[lingeling] 
[lingeling] Copyright (C) 2010-2016 Armin Biere JKU Linz Austria.
[lingeling] All rights reserved.
[lingeling] 
[lingeling] released Sat May 28 15:42:42 CEST 2016
[lingeling] compiled Sat May 28 15:42:42 CEST 2016
[lingeling] 
[lingeling] gcc (Ubuntu 4.8.4-2ubuntu1~14.04) 4.8.4
[lingeling] -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
[lingeling] -DNLGLFILES -DNLGLDEMA
[lingeling] Linux cluster2 3.13.0-63-generic x86_64
[lingeling] 
[exists>slvfun] 1212 AIG vars, 10759 AIG ands, 9123 CNF vars, 25253 CNF clauses
[exists>slvfun] SAT call 1 returned 20 in 0.016 seconds
unsat
[btor>smt2] parsed 8 commands in 0.77 seconds
[btor>parse] parsed 0 inputs and 0 outputs
[btor>parse] logic BV
[btor>parse] status unsat
[btor>core] 0/0/1/0 constraints 0/0/1/0 0.1 MB
[btor>core] variable substitutions: 0
[btor>core] uninterpreted function substitutions: 0
[btor>core] embedded constraint substitutions: 0
[btor>core] assumptions: 0
[btor>core] memory allocated for nodes: 0.08 MB
[btor>core] 
[btor>core] bit blasting statistics:
[btor>core]  AIG vectors (cur/max): 0/0
[btor>core]  AIG ANDs (cur/max): 0/0
[btor>core]  AIG variables: 0
[btor>core]  CNF variables: 0
[btor>core]  CNF clauses: 0
[btor>core]  CNF literals: 0
[btor>core] 
[btor>core] linear constraint equations: 0
[btor>core] gaussian elimination in linear equations: 0
[btor>core] eliminated sliced variables: 0
[btor>core] extracted skeleton constraints: 0
[btor>core] and normalizations: 0
[btor>core] add normalizations: 0
[btor>core] mul normalizations: 0
[btor>core] lambdas merged: 0
[btor>core] apply propagation during construction: 0
[btor>core] beta reductions: 0
[btor>core] clone calls: 0
[btor>slvef] 
[btor>slvef] cegqi solver refinements: 1
[btor>slvef] cegqi solver failed refinements: 0
[btor>core] 
[btor>core] 0.00 seconds beta-reduction
[btor>core] 0.00 seconds synthesize expressions
[btor>core] 0.00 seconds determining failed assumptions
[btor>core] 0.00 seconds for cloning
[btor>core] 0.00 seconds beta reduction probing
[btor>core] 0.00 seconds substitute and rebuild
[btor>core] 
[btor>core] 0.00 seconds in rewriting engine
[btor>core] 0.00 seconds in variable substitution during rewriting (0%)
[btor>core] 0.00 seconds in embedded constraint replacing during rewriting (0%)
[btor>core] 0.00 seconds in apply elimination during rewriting (0%)
[btor>core] 0.00 seconds skeleton preprocessing during rewriting (96%)
[btor>slvef] 0.02 seconds exists solver
[btor>slvef] 0.74 seconds forall solver
[btor>slvef] 0.00 seconds synthesizing functions
[btor>slvef] 0.00 seconds find partial model
[btor>slvef] 0.00 seconds quantifier instantiation
[btor>slvef] 0.00 seconds check instantiation
[btor>core] 
[btor>core] 0.1 MB
[btor>main] 0.8 seconds process
[btor>main] 0.8 seconds real
[btor>main] unsat
c launch: done
