assert is_uninterpreted (decl) in fp_get_preds function (utils.py)

[ploc]

I have the following error on this benchmark kind_fmcad08/large/steam_boiler_no_arr2_e6_3003_e4_15091

I first generate the smt2 without errors from lustrec.

Then zustre fails:
$ zustre --smt2 steam_boiler_no_arr2_e6_3003_e4_15091.smt2
[INFO] 2017-07-13 10:22:49,814 zustre 165 [No pre-processing ]
[INFO] 2017-07-13 10:22:49,814 zustre 180 [Successful Horn Generation ... steam_boiler_no_arr2_e6_3003_e4_15091.smt2 ]
Process Process-1:
Traceback (most recent call last):
File "/usr/lib/python2.7/multiprocessing/process.py", line 258, in _bootstrap
self.run()
File "/usr/lib/python2.7/multiprocessing/process.py", line 114, in run
self._target(*self._args, **self._kwargs)
File "/home/ploc/Local/zustre/bin/zustre", line 76, in main
zus.encodeAndSolve()
steam_boiler_no_arr2_e6_3003_e4_15091.lus.txt

File "/home/ploc/Local/zustre/lib/zustrepy/src/zustre.py", line 182, in encodeAndSolve
preds = utils.fp_get_preds(self.fp) # get the predicates before z3 starts playing with them
File "/home/ploc/Local/zustre/lib/zustrepy/src/utils.py", line 51, in fp_get_preds
assert is_uninterpreted (decl)
AssertionError

Note the a direct call to spacer/z3 is OK:
$ z3 steam_boiler_no_arr2_e6_3003_e4_15091.smt2
unsat

[agurfinkel]

The input must contain a rule of the form
(=> phi (P ...) )
where P is not an uninterpreted predicate. Perhaps you have a rule
(=> phi false)
I can't tell without the input file.

[ploc]

The input file is attached. Do you need the smt2 file?

[agurfinkel]

Yes, the smt2 file since this is what is causing the problem.

[ploc]

steam_boiler_no_arr2_e6_3003_e4_15091.smt2.txt