% EXPECT: unsat