Could nunchaku be used for Coq (which allows empty types)?

[samuelgruetter]

As pointed out by @blanchette, nunchaku is based on a theory where all types are inhabited.
In Coq, however, empty types are allowed, and it's more than a theoretical curiosity required to define False, but it's actually a feature I use in my work: I'm writing a compiler which does not yet support function calls, while my colleague is writing a separation logic framework for its input language which already supports function calls, and in order to share the same ASTs, we generalize the AST over function names, and he instantiates them with string, while I instantiate them with the empty type, as illustrated in this minimized example:

Require Import Coq.Lists.List. Import ListNotations.

Inductive stmt{varname funcname: Type}: Type :=
| SAdd(res arg1 arg2: varname)
| SSet(x: varname)(v: nat)
| SCall(f: funcname)(res: varname)(args: list varname).

Definition collect_varnames{V F}(s: stmt (varname:=V) (funcname:=F)): list V :=
  match s with
  | SAdd res arg1 arg2 => [res; arg1; arg2]
  | SSet x v => [x]
  | SCall f res args => res :: args
  end.

Inductive empty_funcname: Type := .

Definition simple_stmt := stmt (varname:=nat) (funcname:=empty_funcname).

Lemma number_of_vars_bound: forall (s: simple_stmt),
    length (collect_varnames s) <= 2.
Proof.
  (* call counterexample generator here *)

Here, a counterexample generator should report a counterexample for the SAdd case (because 3 <= 2 does not hold), and it should not report a counterexample based on the SCall case, because that's impossible for simple_stmt.

Now I wonder wether/how this could be encoded in nunchaku.

data empty_funcname := . 

doesn't work because it results in a parsing error.

val empty_funcname: type.

axiom forall (fn: empty_funcname). false.

doesn't work either because nunchaku considers it UNSAT.

Given that a Coq plugin for nunchaku was started, I guess it was assumed that this could be made working somehow? If so, how?

I'm not restricted to sound and complete solutions, I'd also be interested in "practical" solutions 😉