Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.

* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line

Merge branch '1.3.x'

Fix to interactive mode determination.

Fix option specification.

Merge branch '1.3.x'

[skip ci]

Fix an autoconf issue with CLN in some configurations; also clarification re: license issues

[skip ci]

Merge branch '1.3.x'

Fix configure handling for CLN (should fix win32 nightly builds)

Merge branch '1.3.x'

Reduce autoconf version for dependence (should fix 32-bit builds).

Add missing regression-results directory.

Merge branch '1.3.x'

configure --with-portfolio disables CLN.

Merge branch '1.3.x'

Conflicts:
COPYING
NEWS

some config changes: new --bsd option, readline gives warning, default build is now production.

First attempt at incorporating LFSC proof checker into CVC4.

Merge branch '1.3.x'

Send Travis-CI emails to everyone

Merge branch '1.3.x'

Fix for bug 544.

Merge branch '1.3.x'

Another fix for clang.

Merge branch '1.3.x'

Fix stack size on in-tree regressions.

cleanup

Merge branch '1.3.x'

Fix link error when using clang.

Fix to Travis-CI config.

Fix to Travis-CI config.

Merge branch '1.3.x'

Travis-CI configuration.

Some minor cleanup.

Update NEWS.

Merge branch '1.3.x'

Fix timer statistics to report correct time even on process abort.

Whitespace.

Fix warning.

Remove "NodeValue width" output

GLPK build identifier, license warnings.

Fix timer statistics to report correct time even on process abort.

Whitespace.

Fix warning.

Remove "NodeValue width" output

GLPK build identifier, license warnings.

Merge branch '1.3.x'

mv prp to regress1

Merge branch '1.3.x'

fix bug 542

Initializing master for next version.

Initializing 1.3.x branch.

Cutting release 1.3.

disable substring in default mode

Fix NodeValue bitfields for 32-bit; fix comment.

Minor cleanup.

Update copyrights, add missing file-level documentation; fix perms.

Fixes related to parametric datatype printing.

Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now works).

Script fixes; when determining authorship of source files, don't count copyright-updating commits.

Fix NEWS.

NEWS reorganization.

Remove a regression for which the portfolio takes forever (see bug 542).

Minor cleanup.

Partial kind branch merge, including new --rewrite-apply-to-const feature.

Don't put define-funs in model output; bug 411 testcase no longer relevant.

Updated acknowledgments.

More Java bindings fixes

Merge branch 'master' of github.com:tiliang/CVC4

adds LB strategy

adds LB strategy

Some fixes for swig warnings.

Merge branch 'master' of github.com:tiliang/CVC4

Last version for undelayed LB

Last version for undelayed LB

Work around a swig segfault issue when building on  Mac OS

change string news

Merge branch 'master' of github.com:tiliang/CVC4

string fmf perfomance fix

string fmf changes

string fmf perfomance fix

rm ChangeLog (use NEWS)

SExpr pretty-printing for :all-options and :all-statistics.

Minor cleanup.

Add test case for (previously resolved) bug 528.

Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a subtype of (Pair Real Real).  Resolves bug #541.

fixed rewriter bug where postRewrite was not caching properly

Another fix to Java destruction order issues.  Thanks to Zheng Manchun for the report.

Update NEWS file.

Fix proofs build.

Fix portfolio compile error.

Ignore config/compile file, which newer autotools create

Fix for compile error when using gcc 4.7 with -std=gnu++11.  Thanks to Martin Brain for the patch!

General pre-release cleanup commit

* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing

Java bindings improvements for CASCADE, minor cleanup.

Add missing template instanatiation in Java bindings

Some versioning in advance of the 1.3 release.

Incremental is now on by default when using from API, off for command-line driver except in interactive mode.

Bug fix for E-matching select terms, minor fix for bounded integers, bug fix to improve performance of quantifiers rewriter

Fix a segfault in the printer infrastructure when called from API and no language is set

Fix C++-to-Java exception translation.

Fix Java output stream adapter.