Cannot get Interpretation of some FuncDecls

[toolCHAINZ]

Noticed while investigating #459

        let solver = Solver::new();
        let f = FuncDecl::new("hi", &[], &Sort::int());
        solver.assert(f.apply(&[]).as_int().unwrap().eq(5));
        solver.check();
        let model = solver.get_model().unwrap();
        let interp = dbg!(model.get_func_interp(&f).unwrap());

This code panics on the unwrap of the final line. The actual model does have an interpretation of f. Since f has an arity of 0, we go into a code-path that uses Z3_get_const_interp and assumes the returned Ast is an Array. In this case, it is an Int and so it fails.

The code around FuncInterp probably needs to be seriously rethought, maybe as an item in #447.