Verification of the following simple example succeeds with only one level. Debugging the backends doesn ot show the consecution calls one would expect to derive the necessary invariant.
Does VVT perhaps simplify this example too much?

dfa.l.zip
dfa.c.zip
(I've skipped the large-block reduction and the transition relation optimizing steps. The latter solves the problem already.)

Some fields in the IC3Stats datatype are not updated as they should for me, for example the function 'elimSpuriousTrans' is entered multiple times during a run, but the corresponding update of 'numRefinements' and 'numAddPreds' is not preformed as intended, they are both 0 in the end of the run when the stats are dumped.

It seems that the fields 'numAbortMic' and 'numAbortJoin' are also affected, as I have never seen a different value from 0 for them when the stats are dumped.

When compiling the entire project (stack clean; stack build) with gcc 5.3.1 linking with bindings-llvm does not work. Following error appears

Compiling with gcc version 4.9.3 works. When bindings-llvm is already compiled, only compiling vvt with gcc 5.3.1 works too.

Mathsat gives the error (error "model generation not enabled") although setOption (ProduceModels True) was called when the SMTPool was created.

The SMTPool is created in the function runIC3 in the file CTIGAR.hs, line 340. The error occurs when adding

curSt <- getValues (interpCur st) >>= TR.renderState (ic3Model cfg)
curInpSt <- getValues (interpInputs st) >>= TR.renderInput (ic3Model cfg)
nxtSt <- getValues (interpNxt st) >>= TR.renderState (ic3Model cfg)
liftIO $ putStrLn $ "State:\n"++curSt++"\nInput:\n"++curInpSt++"\nNext state:\n"++nxtSt                 

in interpolateState (line 1124).