Z3's quantifiers have been replaced by functions which generate finite conjunctions and disjunctions, leading to a massive performance gain. The following new features have also been included:
- The user can specify a `max_time` and is prompted to increase the time if the `model-checker` times out.
- The user can set an `optimize` variable with override flag `-o` to have the model-checker find a model with the smallest number of atomic elements within the `max_time`.
- The user can set the `contingent` variable with override flag `-c` to require all propositions to be contingent, i.e., to have some possible verifier and some possible falsifier. Since the null state cannot verify nor falsify a contingent proposition, constraints on propositions to only have non-null verifiers and falsifiers have been removed.
In addition to these features, the unit tests have been expanded to now include 120 examples which are divided by logical operators.