Description
Hi there,
We have some problems parsing and transforming C files into SMT2 descriptions. Some of these are unprecedented and we believe have emerged after some recent updates. However we can not specifically identify which one.
We ran CBMC with a simple unwinding option of 2 (not involved with unwinding assertions) on fmt source from coreutils-8.23. The goal is to get the program specifications in SMT2. Although the source is not that much long, and it is rather mildly complicated with recursive functions and stuff, but CBMC shoots out by returning a ~30 GB SMT2 file after 3hrs of tedious working. We ran the same setting with DIMACS format which it didn't even bothered giving out a result and failed after SSA conversions. It seems like it can not figure out how to write formulae into a file. We assured that hard disk space is available and the process has enough access for file operation though.
To give you a glimpse of our trail and error, we also ran the same exact settings for wc command which also failed in generating SMT2, and numfmt, which generated a DIMACS file weighting 104 MB but also gave on when it came to SMT2. However, it is not a consistent phenomenon after all. We have successfully generated SMT2 files of 100 MB or less for some of the other sources in that package. Nevertheless, there were cases where we have got a sound SMT2 file before but now it seems that sometimes the returned SMT2 formulae is partial or half-cut, since Z3 complains about parsing those files.
Just asking anyway, is it normal for an SMT2 file to be like multiple Gigabytes? Even though for such a cute, tiny, number of unwinding turns?