Shaping Formal Traces without Constraints: A Case Study in Closing Code Coverage on a Crypto Engine Using Formal Verification