Add simplification option --fo-prop-quant.  Add model support for new model-checking procedure.  Add run script for casc24-fnt.
Add documentation for --disable-fmf-inst-gen, which removes a warning
Fix erroneous results when the logic was incorrectly specified (by throwing LogicException).  Also correct a case where sharing was doing some work during pure theory solving.
fixes to the proof system so it works with theory lemmas and explanations
Update casc run script.  Work on compliance for SZS output.
now proofs print mapping between atom and propositional variable as a comment in LFSC
disable Logic-checking with finite model finding for now, since FMF uses Rationals, making the check think arithmetic should be enabled (but it's not)
Preliminary version of finite model finding over bounded integer quantification. Minor update to casc script.
Refactoring to separate old and new model building/checking code.
Add support for quantifier patterns in smt2 printer.
added some extra options to the bit-vector theory
Update casc24-fnt run script.  Add casc24-fof run script.
minor changes to language bindings
Fix minor bug in full_model_check.cpp
configure fix for building with glpk on redhat, perhaps others
Fix to empty response to (get-assignment).

Thanks to David Cok for reporting this issue.
Fixed "success" response to (push N) / (pop N) with N > 1.

Thanks to David Cok for reporting this issue.
Disallow construction of (_ BitVec 0).

Thanks to David Cok for reporting this issue.
A couple of fixes to the get-option command for compliance with SMT-LIB.

Thanks to David Cok for reporting this issue.
Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places

Thanks to David Cok for reporting these issues.