--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on May 2020 ---
Hello Mike, > > For different solvers, I get different answers from alt-ergo and z3 for the same properties, with z3 timing out or failing on a handful of goals that alt-ergo succeeds on. I would expect differences in timeouts between solvers (e.g., one times out but not the other), but not discrepancies as to whether obligations are true or false. Perhaps âfailureâ in this case simply means âfailure to proveâ. I am running z3 4.8.4 and alt-ergo 2.3.2. It is very important to understand and accept that in general, as you suspect, âfailureâ means 'failure to proveâ. This is related to very fundamental facts about mathematical logic and computer science and constitutes one of the greatest scientific achievements of the 20th century. I just link to this paragraph of a wikipedia article on automated theorem probing https://en.wikipedia.org/wiki/Automated_theorem_proving#Decidability_of_the_problem The book "Logic in Computer Science: Modelling and Reasoning about Systemsâ by Michael Huth and Mark Ryan also has a short section about this topic. (The book is is available at Amazon: https://www.amazon.com/Logic-Computer-Science-Modelling-Reasoning/dp/052154310X) Regards Jens