As mentioned in the Wiki on Dafny GitHub, when Dafny cannot prove an assertion in a program, it might be due to either my program is incorrect OR the incompleteness of Dafny. But I figured the counter example from Dafny is spurious after I tried understanding it, so I still have no idea if my program is correct or not.
My question is as follows.
If I manage to use another Boogie backend such as Corral to check the translated Boogie program from Dafny using /print, and Corral also returns a model to invalidate the Boogie program, would that guarantee the model disprove my Dafny program and I can use it for debugging? Or is it still likely spurious so don't bother to try it?
From their papers, it seems to me that Corral and Symbooglix should guarantee that a provided model should be a concrete counter example for the translated Boogie program, so maybe my question is more on whether the Dafny program and the translated Boogie program is semantically equivalent.
PS: I tried passing translated bpl files to Corral and check specific Boogie procedure in that bpl, and Corral simply says it cannot find the procedure, so I'm debating if I want to make it work.
It's unlikely that another backend will have any better luck with the translated Boogie file, because the reasons for incompleteness are fundamental.
For example, Dafny ships an axiomatization of several data structures, including sequences, and these axiomatizations are known to be incomplete.
If you are having trouble with understanding a specific Dafny failure, I suggest you ask another question about your specific program and include a minimal working example, if possible.