In my C compiler rcc I throw compile-time errors of course. Not a full SMT solver like z3, just a self written solver, but it works fine and fast enough. Runtime errors are just glorified asserts, lame.