One source of Z3 spurious counterexamples is this: Z3 can return a model for an array in a variety of different ways. In each case it represents the model as an AST. We handle some of these ASTs but not all of them.
In practice, it seems that the technique we have now works most of the time, especially for identifying the initial state of the bad counterexample. It works less often for identifying that bad state of the target/rewrite programs.
To actually fix this would take some work to understand all the possible AST nodes that Z3 could use and to write a recursive function to parse them out. There's also the possibility that Z3 won't return concrete values for the entire array and we'd have to fill in something on our own (although I'm not sure I've seen this myself).
If ever someone is trying to troubleshoot such an issue, take a look at z3solver.cc. There's a check as follows:
ok &= Z3_get_decl_kind(context_, array_eval_func_decl) == Z3_OP_AS_ARRAY;
If ever 'ok' is false, then our counterexample is probably spurious and a more advanced technique is needed to correctly extract the model.
One source of Z3 spurious counterexamples is this: Z3 can return a model for an array in a variety of different ways. In each case it represents the model as an AST. We handle some of these ASTs but not all of them.
In practice, it seems that the technique we have now works most of the time, especially for identifying the initial state of the bad counterexample. It works less often for identifying that bad state of the target/rewrite programs.
To actually fix this would take some work to understand all the possible AST nodes that Z3 could use and to write a recursive function to parse them out. There's also the possibility that Z3 won't return concrete values for the entire array and we'd have to fill in something on our own (although I'm not sure I've seen this myself).
If ever someone is trying to troubleshoot such an issue, take a look at z3solver.cc. There's a check as follows:
ok &= Z3_get_decl_kind(context_, array_eval_func_decl) == Z3_OP_AS_ARRAY;If ever 'ok' is false, then our counterexample is probably spurious and a more advanced technique is needed to correctly extract the model.