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.
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)
minor changes to language bindings
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.
Better error on invalid logic strings.

Thanks to David Cok for reporting this issue.

Conflicts:
	library_versions
Fix destruction issue in GetValueCommand leading to crash.

Thanks to David Cok for reporting this.
Fix for equality-chaining of Booleans in SMT-LIBv2.

Thanks to David Cok for reporting this.
As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => takes n>2 args and is right-assoc.

Thanks to David Cok for pointing out this issue.
Don't allow get-model & co after a user push/pop

This makes us more strictly adhere to the spec, but it's useful anyway:
previously we would support a get-model until the problem was explicitly
changed with e.g. a new assertion.  That meant you could check-sat, then
pop, then get-model, but you'd only get the part of the model still in
scope.  This is strange, and would likely lead to problems, so it's now
disabled.

Thanks to David Cok for inquiring about this.
Compliance fixes for :named annotations: they must name closed subterms, the names must be user-permitted names, etc.

Thanks to David Cok for raising this issue.
Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive mode.

Thanks to David Cok for raising this issue.
Detect multiply-defined :named annotations and issue an error.

Thanks to David Cok for pointing out this issue.

Conflicts:
	library_versions
Update THANKS to mention David Cok's contributions.
Fix error reporting on use of (nonlinear) div,mod,/ symbols