When BDDs Fail: Conformance Testing with Symbolic Execution and SMT Solving