More useful error message when someone tries mkExpr(VARIABLE).
Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).
Guard java-specific swig code with SWIGJAVA.

Without this building just the python bindings will fail.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Improving support for POW in arithmetic. Resolves bug 549.
Don't tokenize SET_THEORY operators in smt2 parser
Revert "fix naming conflicts in benchmarks"

This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.
Array smtlib compliance tests
Merge pull request #14 from kbansal/sets-parserchanges

Sets parserchanges
adds incremental for strings; clean-up codes
adds incremental for strings; clean-up codes
Merge branch 'master' of github.com:tiliang/CVC4
Add swig renames for new Z3STR language.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Fix strings-exp setting.
bring back D-Norm
remove unrolling depth
Fix strings-exp setting.
bring back D-Norm
remove unrolling depth
Merge branch 'master' of github.com:tiliang/CVC4
Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master.  See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.