Z3 exception with an empty subclass

[dijkstracula]

Given the following simplified code:

123     class man_msg_t = {
124         action handle(self: manager_id, ^msg: man_msg_t)
125     }
126
...
154
155     # An unpark message is sent to a node when execution can resume.
156     subclass unpark of man_msg_t = {
157         action handle(self: manager_id, ^msg: unpark)
158     }

Ivy throws the following z3 exception:

~/code/ivy-ts(main ✗) make
cd src/; ivyc target=test server.ivy
Traceback (most recent call last):
  File "/Users/ntaylor/bin/ivyc", line 11, in <module>
    load_entry_point('ms-ivy', 'console_scripts', 'ivyc')()
  File "/Users/ntaylor/code/ivy/ivy/ivy_to_cpp.py", line 5641, in ivyc
    main_int(True)
  File "/Users/ntaylor/code/ivy/ivy/ivy_to_cpp.py", line 5775, in main_int
    header,impl = module_to_cpp_class(classname,basename)
  File "/Users/ntaylor/code/ivy/ivy/ivy_to_cpp.py", line 2873, in module_to_cpp_class
    emit_action_gen(sf,impl,name,action,classname)
  File "/Users/ntaylor/code/ivy/ivy/ivy_to_cpp.py", line 1201, in emit_action_gen
    impl.append('add("(assert {})");\n'.format(slv.formula_to_z3(pre).sexpr().replace('|!1','!1|').replace('\\|','').replace('\n',' "\n"')))
  File "/Users/ntaylor/code/ivy/ivy/ivy_solver.py", line 599, in formula_to_z3
    z3_fmla = formula_to_z3_closed(fmla)
  File "/Users/ntaylor/code/ivy/ivy/ivy_solver.py", line 588, in formula_to_z3_closed
    z3_formula = formula_to_z3_int(fmla)
  File "/Users/ntaylor/code/ivy/ivy/ivy_solver.py", line 557, in formula_to_z3_int
    args = [formula_to_z3_int(arg) for arg in fmla.args]
  File "/Users/ntaylor/code/ivy/ivy/ivy_solver.py", line 557, in formula_to_z3_int
    args = [formula_to_z3_int(arg) for arg in fmla.args]
  File "/Users/ntaylor/code/ivy/ivy/ivy_solver.py", line 557, in formula_to_z3_int
    args = [formula_to_z3_int(arg) for arg in fmla.args]
  File "/Users/ntaylor/code/ivy/ivy/ivy_solver.py", line 557, in formula_to_z3_int
    args = [formula_to_z3_int(arg) for arg in fmla.args]
  File "/Users/ntaylor/code/ivy/ivy/ivy_solver.py", line 554, in formula_to_z3_int
    return atom_to_z3(fmla)
  File "/Users/ntaylor/code/ivy/ivy/ivy_solver.py", line 464, in atom_to_z3
    return apply_z3_func(pred,tup)
  File "/Users/ntaylor/code/ivy/ivy/ivy_solver.py", line 346, in apply_z3_func
    fact = z3_to_expr_ref(z3.Z3_mk_app(pred.ctx_ref(), pred.ast, sz, _args), pred.ctx)
  File "/Users/ntaylor/code/ivy/ivy/z3/z3core.py", line 1565, in Z3_mk_app
    _elems.Check(a0)
  File "/Users/ntaylor/code/ivy/ivy/z3/z3core.py", line 1336, in Check
    raise self.Exception(self.get_error_message(ctx, err))
ivy.z3.z3types.Z3Exception: Sort mismatch at argument #2 for function (declare-fun |*>:manager.man_msg_t:manager.unpark|
             (manager.man_msg_t manager.unpark)
             Bool) supplied sort is Int
make: *** [src/server] Error 1
~/code/ivy-ts(main ✗)

Adding an unused field in the subclass alleviates the issue, however.