scratchpad::test_utils::naive_smt