add redmine example

[izgzhen]

However, this example makes the cozy stuck now

cozy examples/redmine.ds --java Redmine.java --simple
Checking call legality...
Checking invariant preservation...
Checking that insertIssue preserves (unique Map {p -> ((p).val).id} (projects))...
Checking that insertProject preserves (unique Map {p -> ((p).val).id} (projects))...
Checking that updateProjectStatus preserves (unique Map {p -> ((p).val).id} (projects))...
Done!
Adding query countIssues...
Adding query _query3818...
Adding query _query3819...
Adding query getProjectById...
Adding query _query10402...
Adding query _query10403...
Setting up handle updates for insertIssue...
Setting up handle updates for insertProject...
Setting up handle updates for updateProjectStatus...

Stuck in the last line without any output for a long time

[izgzhen]

@Calvin-L

[izgzhen]

it works!

WARNING: took 216.95123s to solve

[Calvin-L]

For once, it really does seem to be Z3 taking a long time.

Handles are very expensive to reason about. I don't recommend using them for immutable types like IssueStatus or ProjectModule, if you can get away with it.

Also, there are many invariants that this specification omits. For instance, every project referenced by an issue must be in the set of projects, no?

[izgzhen]

For instance, every project referenced by an issue must be in the set of projects, no?

I think so. I might need to revise these examples later.