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.