#2 Syntax error on Why-generated text

[David A. Wheeler]

The program "Why" can generate SMT-LIB verification conditions from source code, but the DPT seems to choke on them. What's worse, it just says: "Fatal error: exception Parsing.Parse_error"

Notice the lack of line#, never mind column#. Eeek. Not much to go on.

I've installed an "smtlib" directory with "logics" and "theories" subdirs, which contain:
./logics:
AUFLIA.smt

./theories:
Int_ArraysEx.smt

I generated an .smt file using "Why"'s binary-search.c file, and ran DPT's smtlib_solver this way:
~/Download/dpt-1.2/bin/smtlib_solver.opt -l /home/dwheeler/Download/smtlib binary-search_why.smt

Syntax error.

I tried with a simpler swap.c, and still, no dice. I don't know if the problem is with Why, DPT, or something else, but Why's SMTLIB file _does_ work with Yices, so my first guess is DPT.

I'm attaching the binary-search.smt sample.

[David A. Wheeler]

binary-search.smt