…perserver

… into ViperPost, added ProgramDefinitionsProvider.

…generic method VerificationServer.initializeProcess. Fix typos. Add stubs for the AST construction request.

initializeVerificationProcess now takes Future[MessageStreamingTask[AST]]

…rifyPost now completes the /verify request with ast_id and ver_id.

The former can be used for streaming AST construction results.
The latter can be used for streaming the verification results.
(3) Added json writers for AstConstructionResultMessage instances.

- Fixed a bug that resulted in repetition of reported cached messages.
- Fixed a bug that resulted in duplication of reported errors (overall vs. for_entity)
- Fixed a logging bug in doCachedVerification
- Add flag "cached" to the marshalled representation of AbstractError.
- Added stubs for caching functions and predicates

- The HTTP router in VSI is backwards compatible with the old interface: the client can choose whether to submit an /ast/ast_id request or not, all the messages that were produced and not consumed yet (both from AST construction and from verification) will still be streamed via the /verify/ver_id request.
- Fixed a bug with double execution of cleanup tasks after AST construction jobs
- Terminator actor is no longer responsible for cleaning up after individual jobs. The JobPool and its client take care of that at the point of job creation, not at the point of streaming.
- JobHandles are now linked. Added new field `prev_job_id` to VerHandle.
- Important changes in initializeProcess (cleanup after queue is completed, only create job actors if the task can be executed, recover from the case of AST errors in verification jobs)
- getInterruptFutureList now also cleans up AST construction tasks.

….13.4

…n-existent files.

- check for non-existent files in generateViperAst
- streamMessages now returns Option[Future[Done]] rather than Option[Future[Unit]]

…verTest.

…methods.

- Cosmetic edits.

Update Java in build script to version 15

…t ModelEntry

Use pavpanchekha/setup-z3 to get the right version of Z3.

Try to fix the Z3 setup

No need to run sbt assembly for testing.