c launch: /home/mathias/runs/boolector/tacas2016/20161015-boolector-converted-dual-synth=0/benchmarks /home/mathias/runs/boolector/tacas2016/converted/ /home/mathias/runs/boolector/tacas2016/20161015-boolector-converted-dual-synth=0 --time-limit=2400 --space-limit=7000 /home/mathias/runs/boolector/tacas2016/20161015-boolector-converted-dual-synth=0/boolector -v --ef:dual --ef:synth=0
c host: atom15
c benchmark: /home/mathias/runs/boolector/tacas2016/converted/NRA/keymaera/intersection-example-simple.proof-node31665.smt2
c solver: /home/mathias/runs/boolector/tacas2016/20161015-boolector-converted-dual-synth=0/boolector
c solver options: -v --ef:dual --ef:synth=0
[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 '/home/mathias/runs/boolector/tacas2016/converted/NRA/keymaera/intersection-example-simple.proof-node31665.smt2'
[btor>smt2] parsed 25 commands in 0.00 seconds
[btor>slvfun] enabled core engine
[btor>slvfun] calling SAT
[btor>core] 0 rewriting rounds in 0.0 seconds
[btor>core] simplification returned 20
[btor>slvfun] SAT call 1 returned 20 in 0.000 seconds
unsat
[btor>smt2] parsed 27 commands in 0.00 seconds
[btor>parse] parsed 20 inputs and 0 outputs
[btor>parse] logic BV
[btor>parse] status unknown
[btor>core] 0/0/0/0 constraints 0/0/0/0 0.0 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.03 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>slvfun] 
[btor>slvfun] lemmas on demand statistics:
[btor>slvfun]  refinement iterations: 0
[btor>slvfun]  LOD refinements: 0
[btor>slvfun] expression evaluations: 0
[btor>slvfun] propagations: 0
[btor>slvfun] propagations down: 0
[btor>slvfun] partial beta reduction restarts: 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 in slicing during rewriting (0%)
[btor>core] 0.00 seconds skeleton preprocessing during rewriting (0%)
[btor>slvfun] 
[btor>slvfun] 0.00 seconds expression evaluation
[btor>slvfun] 0.00 seconds initial applies search
[btor>slvfun] 0.00 seconds lemma generation
[btor>slvfun] 0.00 seconds not encoded apply search
[btor>slvfun] 0.00 seconds propagation apply search
[btor>slvfun] 0.00 seconds in pure SAT solving
[btor>slvfun] 
[btor>core] 
[btor>core] 0.0 MB
[btor>main] 0.0 seconds process, 38% utilization
[btor>main] 0.0 seconds real
[btor>main] unsat
c launch: done
