[735] % z3 small.smt2
sat
[736] % z3 rewriter.flat=false small.smt2
Failed to verify: lemma->get_pob()->pt().check_inductive(lemma->level(), cube, uses_level, lemma->weakness())
[737] % 
[737] % cat small.smt2
(set-logic HORN)
(assert (exists ((a Int) (b Int) (c Int)) (and (= (* 2 a) b) (or (= (* 1) c) (= 0 b)))))
(check-sat)
[738] %