another DISTCLEANFILES entry, for proper "make distclean" behavior (fixes "distclean" target error last night)
In non-linear logics, rewrite DIVISION, INTS_DIVISION, and INTS_MODULUS into ITEs of the form:

  IF (denom = 0) THEN divByZero(num) ELSE (DIVISION_TOTAL num denom) ENDIF

where divByZero is an uninterpreted function symbol (there's one for each of the partial operators).

In linear logics, don't do any of this.

Bitvector partial functions to come, if this is successful for Tim.

(this commit was certified error- and warning-free by the test-and-commit script.)
Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicException for errors where the user uses a feature not permitted in the current logic (e.g., a quantifier in a QF logic)
Arithmetic problem that fails --check-models due incompleteness with multiplication.
Test that breaks arithmetic model building due to disequality terms.
export null nodes (fixes a bug in portfolio model stuff)
TheoryEngineModelBuilder::buildModel() is only called once with fullModel=true, within a SAT context.  This fixes some outstanding model bugs.

Committing also a Clark-provided assertion the Model code to ensure the call is only done once per context.

(this commit was certified error- and warning-free by the test-and-commit script.)
Finally tracked down problems in regressions and fuzz results (this also
explains why my build was giving different answers from Dejan's build).
Problem was that if you run:

cvc4 --check-models foo.smt

it would fail, but if you run

cvc4 --check-models --produce-models foo.smt

it would succeed.  Even though produce-models is supposed to be automatically
set when you set check-models, it seems this was happening too late.  Fixed by
removing any distinction between produce-models and check-models in the
heuristic setting code.  Kind of ugly though.

Also, disable models if nonlinear arithmetic is on.
fix typo in language bindings
Updates to Clark's commit r4540:

* ALL_SUPPORTED/QF_ALL_SUPPORTED don't include nonlinear
* Change "Notice" to "Warning" when produce-models turned off due to non-linear

(this commit was certified error- and warning-free by the test-and-commit script.)
Change run-regression script to *additionally* run a second test with --check-models *if* the benchmark is sat/invalid (or is incremental, with at least one sat/invalid result).

This increases significantly the time to do a "make regress", as more tests are running.

We need to run both *with* and *without* --check-models, since that option disables certain preprocessing.

To turn off these extra tests during a make regress, you can set CVC4_REGRESSION_ARGS=--no-check-models.

To turn off the extra test for a *particular* regression benchmark, you can put this in the benchmark:

; COMMAND-LINE: --no-check-models

That might be necessary in e.g. nonlinear arithmetic benchmarks.

(this commit was certified error- and warning-free by the test-and-commit script.)
Fix for bug 439. Delta computation now includes disequality information.
Fixed missing \ in uflra/Makefile.ma
Fixed another model bug and added previously failing fuzz testcase
Removing rewriter call in SmtEngine::addFormula().
Fix to quantifier rewritting not being idempotent. See bug 441.
Beautifying integer_cln_imp.h
Fixes for the arithmetic normal form and rewriter to handle arbitrary constants for total functions.
minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver
* Fix language bindings: various issues
** remove a number of warnings in bindings generation
** give appropriate names for operator-overloading
** make sure Java language bindings are built with -fno-strict-aliasing, to ensure the optimizer doesn't produce bad code

* Also remove BitVector::equals(), which wasn't used and was inconsistently implemented (operator==() is still there).

(this commit was certified error- and warning-free by the test-and-commit script.)
Fix for bug 444, dealing with the placing of set-logic in dumping modes.
CVC4 now produces equivalent output when dumping the SMT1 and SMT2 attachments to that bug report.

This also fixes a memory leak in the new-variable-notification mechanism.

(this commit was certified error- and warning-free by the test-and-commit script.)