Versions, syntaxes ("z3 crashed and produced no output")

Nov 5, 2010 at 11:32 AM
Edited Nov 5, 2010 at 11:34 AM

Hi all,

it looks that current vcc crashes on old syntax (or perhaps invalid includes):


$ cat test.c 
#include "vcc.h"
void test() {};
$ vcc test.c 
Verification of test caused an exception "z3 crashed and produced no output".
Exiting with 3 (1 error(s).)~$ vcc /version
$ vcc /version
Microsoft Research Vcc Version 2.1.31105.0
Microsoft Research Boogie Version 2.1.21027.0
Microsoft Research Z3 Version

What is the recommended last version to use for the old (2009-mid 2010) syntax?


Nov 5, 2010 at 7:46 PM

The old syntax is still fully supported and not the cause of your problem (as z3 does not even report its version number). Why z3 does not run, I don't know, but try running it directly and see if it reports some error.



Nov 7, 2010 at 11:08 AM
Edited Nov 7, 2010 at 8:27 PM

Hi Stephan, yes (having done a reinstall today), z3 now does report a valid version number and everything looks perfect :-)

(Addendum: having done some forensics (the reinstall was on another machine so I still had to fix the original one), it was a vcomp100.dll that hat been missing from "c:\windows\system32" - this vcomp100.dll that recent versions of z3 apparently depend on can be found e.g. in the Microsoft Visual C++ 2010 Redistributable Package.)