Patent Document ID: 9767412
Application ID: 14477735
Patent Flag: 1

Claim One:
1. A method comprising: obtaining, via analysis of each execution path of programming code stored in a local storage device, an SMT formula having a plurality of SMT variables from the programming code; obtaining a simplified SMT formula from the SMT formula, the simplified SMT formula including a plurality of simplified SMT variables; obtaining an SAT formula from the simplified SMT formula, the SAT formula including a plurality of SAT variables; determining, via at least one processor, which of the plurality of the SMT variables are “don't care” variables using the simplified SMT formula; determining, via the at least one processor, which of the plurality of the SMT variables are “don't care” variables using the SAT formula; and using the “don't care” variables determined based on each of the simplified SMT formula and the SAT formula to determine whether an error exists in the programming code.