CVC4/5 unsupported feature shows an error even though another solver is verifying the VC

[samuelchassot]

When using this feature unavailable of CVC4/5, an error message is displayed even though the VC is verified by another available solver. This could be a message displayed only in debug level of logs.

[ Error  ] {* -> mapDefault$14}@?:? (of class inox.ast.Expressions$FiniteMap) is unsupported by solver smt-cvc5:
[ Error  ]   Cannot encode map with non-constant default value

[vkuncak]

Is this reporting fixed now, @samuelchassot ? If not, does it appear only with a debug option? Should we do a check beforehand that the feature does not appear, to save CPU time? Is it the same for cvc4 and cvc5 ? Should this issue be moved to Inox ?

[samuelchassot]

No, it's not. We had a look with Mario some time ago, and it is not easy to change to a warning. When do you mean when you say "beforehand"? yes it is the same for cvc5 and CVC4, and yes, it happens in Inox, so we can move it to Inox.