Warn about trivially spurious conter-example
The given counter-example is given by CVC4:
module FF use real.Truncate use real.RealInfix use int.Int lemma floor: forall x. x <. 1. -> floor x = 0 (* x = 0.0 *) end
But CVC4 will immediately prove the validity of the goal,
goal: forall x. x = 0.0 -> x <. 1. -> floor x = 0 . So it would be great if after getting a counter-example we could send the instantiated goal back to the prover. If it proves the validity of the goal we can add a warning to the user that the counter-example is misleading and that it is a wrong counter-example. It is similar to one iteration of a CEGAR loop.