--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on November 2013 ---
Hi folks, Thanks for helping with the preprocessor problems! I am now running into a different strange issue and I hope there might again be an easy fix. I am simply trying to verify the insertion sort code from here: http://proval.lri.fr/gallery/InsertionSortACSL.en.html Using Frama-C Nitrogen-20111001 from an Ubuntu package, all goals can be proved. However, I am left with many unproved goals using these tools: frama-c-Fluorine-20130601 why-2.33 why3-0.81 Specifically, CVC4 1.1, Z3 4.3.1, and Yices 1.0.39 are all timing out for most (but not all) goals. I've put a screenshot here if that is helpful: http://www.cs.utah.edu/~regehr/frama-c.png I'm running on a fast machine (Intel i7 4770) with plenty of RAM. Of course I could back off and use the older version, but that isn't any fun. Thanks, John