[700] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/tactic/tactical.cpp
Line: 113
r1_size > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[701] % 
[701] % cat small.smt2
(set-option :sat.local_search true)
(set-option :ackermannization.sat_backend true)
(set-option :sat.xor.solver true)
(set-option :ackermannization.inc_sat_backend true)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (xor (xor (xor a (xor a b))) b))
(check-sat-using (then qfufbv_ackr simplify))
[702] %