Despite RefinementSolver output a correct PASS/FAIL result, some edges of a candidate execution are missing in the summary and in the execution graph, which might be confusing for the end user.
Example
AssumeSolver
java -jar dartagnan/target/dartagnan.jar dartagnan/src/test/resources/spirv/patterns/MP-rel2rx.spv.dis cat/spirv.cat --method=eager`
======= CAT specification violation found =======
Flag racy
E29 / E16 @unknown / @unknown
E16 / E29 @unknown / @unknown
=================================================
FAIL
RefinementSolver
java -jar dartagnan/target/dartagnan.jar dartagnan/src/test/resources/spirv/patterns/MP-rel2rx.spv.dis cat/spirv.cat --mehtod=lazy
======= CAT specification violation found =======
Flag racy
E29 / E16 @unknown / @unknown
=================================================
FAIL
Also, edges of other relations are missing in the execution graph (see attachments).
MP-rel2rx-eager.spv.txt
MP-rel2rx-lazy.spv.txt
Despite RefinementSolver output a correct PASS/FAIL result, some edges of a candidate execution are missing in the summary and in the execution graph, which might be confusing for the end user.
Example
AssumeSolver
RefinementSolver
Also, edges of other relations are missing in the execution graph (see attachments).
MP-rel2rx-eager.spv.txt
MP-rel2rx-lazy.spv.txt