; Automatically generated by map2smt (set-logic HORN) (declare-fun new1 (Int Int) Bool) (declare-fun ff () Bool) (assert (forall ( (A Int) (B Int) ) (=> (and (= A 0) (new1 A B) ) ff ) ) ) (assert (not ff)) (check-sat)