Programs that have loops return verified when they shouldn't be. See simple-io.vcy and simple-vector.vcy. Running the following:
src/vcy.exe verify veracity2g/benchmarks/global_commutativity/simple-io.vcy
returns:
Condition at veracity2g/benchmarks/global_commutativity/simple-io.vcy:[2.5-2.124] verified as correct: fname_2 != fname_3 && fname_1 != fname_4 && fname_2 != fname_4
Complete status: true` output
Suggested Fix: Use unknown instead of true when loops are replaced with no ops.
Programs that have loops return verified when they shouldn't be. See simple-io.vcy and simple-vector.vcy. Running the following:
src/vcy.exe verify veracity2g/benchmarks/global_commutativity/simple-io.vcyreturns:
Suggested Fix: Use unknown instead of true when loops are replaced with no ops.