Assert error in Literals.ml when calling E with trivial goal
Closed this issue · 3 comments
When calling zipperposition (main branch) with the following options:
./zipperposition.exe --try-e [e-prover binary] --e-call-point 0.0 -t 30
on the following tptp file:
tff(goal, conjecture, ($true)).
It returns an assert error line 283 in Literals.ml
It seems that this is due to the Literals.Conv.to_tst function being called on an empty clause in eprover_interface.ml (line 136).
To the best of my understanding, since we have an empty clause, the assert false could be replaced by a false TypedSTerm:
| [] -> TypedSTerm.app_builtin ~ty Builtin.false_ []
this has fixed the problem for me, but I'm wary of the assert false being there in order to signal a soundness issue.
Sorry for the late reaction. Could you create a pull request? I'd be happy to merge it.
I assume the assert false is there because an empty clause would usually terminate the prover immediately. With --e-call-point 0.0 that does not happen, which is not ideal but acceptable, I think. I don't think you can get this issue with values larger than 0.0, can you?
Yes, I can make a pull request.
That's exactly what happens, if the prover is allowed to run any amount of time, it terminates instantly.