ASSERTION VIOLATION: File: ../src/ackermannization/ackr_model_converter.cpp, Line: 49

[zhendongsu]

[550] % z3release small.smt2
unknown
[551] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/ackermannization/ackr_model_converter.cpp
Line: 49
!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[552] % cat small.smt2
(declare-fun a () Int)
(assert (= a 0))
(check-sat-using (then sat qfufbv_ackr horn-simplify))