Ok, fair point. One method already exists, I'll just have to create the other one. 

Oh, I'm afraid I have confused you with isBool(val(X, B) > 0), which is not what I generate. Sorry for that, it's a little late for me...
The actual thing I'm generating in that case is just:
isInt(n) /\ checkSat(n > 0 /\ notBool(n=/=0)) == "unsat"

However, if you have a function which has the smtlib attribute when defined in K then that function can be sent to the solver. Let us consider that function being the greatest common divisor - gcd. Then from the path condition n > 0 and the rule condition gcd(A, B) > 0 /\ n =/= 0 /\ isInt(n) I have to generate:

isInt(n) /\ isInt(A) /\ isInt(B) /\ checkSat(n > 0 /\ notBool(gcd(A, B) >0 /\ n=/=0)) == "unsat"