BUG: unverified step
Preliminary Results
Bugs appear to be in the simplify circuit code
Commands
-solver cplex_v3 -reduction fromsat -verify_steps -debug -run solve -locked ../data/dac12/enc05/c2670_enc05.bench !e
-solver cplex_v2 -reduction fromsat -verify_steps -debug -run solve -locked ../data/dac12/enc05/c2670_enc05.bench !e
Error
[LL_CPLEX_DiffCircuit.verify #1]:[**SEVERE] [VerifyStep] The ILP Outputs do not match the Circuits Outputs
input: 01011010111000100000000000011100101001110001110100000111101110011110010111011001001000100000000011010000011000000100000000000000000000000000000000000000000000000000000000000000000000000000001000011000000111111101011111110111110101111
Key_a: 011011110101000101010101110100110101110111111001110100000110
Key_b: 111010010011001101111100111111011111010011000100011110111110
Circuit_Output_a: 1110000010001111001101001010001011101011110000000111010100000001
ILP_Output_a: 1110000010001111001101001010001011101011110000000111010110000001
Incorrect Wires_a:
* Incorrect Output Wire[56]: G395 {output_a: 0, ilp_output_a:1}
Circuit_Output_b: 1110000010001111001101001010001011101011110000000111001100000001
ILP_Output_b: 1110000010001111001101001010001011101011110000000111001110000001
Incorrect Wires_b:
* Incorrect Output Wire[56]: G395 {output_b: 0, ilp_output_b:1}
Circuit Output Difference:
* Expected Output Wire[53]: G311 {output_a: 1, output_b:0}
* Expected Output Wire[54]: G150 {output_a: 0, output_b:1}
2019/08/07 00:12:25.628 - [shahen.logiclocking.circuit.solver.LL_CPLEX_Solver_v3.verify_keys #1]:[ FINE] Verifying 8 Equal Circuits.
2019/08/07 00:12:25.638 - [shahen.logiclocking.circuit.solver.LL_CPLEX_Solver_v3.verify_keys #1]:[ FINE] [VerifyStep] Equal Circuits Verified.
2019/08/07 00:12:25.638 - [shahen.logiclocking.circuit.solver.LL_CPLEX_Solver_v3.input_different_from_previous #1]:[ FINE] [VerifyStep] Distinguishing Input is Different from Previous
2019/08/07 00:12:25.638 - [shahen.logiclocking.options.run.LL_Solve.run #1]:[**SEVERE] shahen.logiclocking.LL_Exception: [Iteration Stage07] Step's results are INCORRECT!
at shahen.logiclocking.circuit.solver.LL_CPLEX_Solver_v3.solve_for_new_distinguishing_input(LL_CPLEX_Solver_v3.java:321)
at shahen.logiclocking.circuit.solver.LL_CPLEX_Solver_v3.solve(LL_CPLEX_Solver_v3.java:116)
at shahen.logiclocking.options.run.LL_Solve.run(LL_Solve.java:49)
at shahen.logiclocking.LL_ILPInstance.run(LL_ILPInstance.java:201)
at shahen.logiclocking.LL_ILPCUI.main(LL_ILPCUI.java:90)