Merge tag 'smtcomp2014-application'

Conflicts:
contrib/run-script-smtcomp2014-application
src/main/driver_unified.cpp

QuitCommand needs "success" output for trace executor. :-(

Final fixes for smtcomp2014-application.

Merge pull request #39 from mdeters/bv-warnings

Fix compiler warnings in BV-related code (unused vars mostly).

Merge pull request #35 from mdeters/bv-kinds

Bit-vector kinds documentation

Another updated submission strategy.

Another updated submission strategy.

Run in application track with --check-models.

Fix compiler warnings (mostly unused variables).

API documentation improvements.

Run in application track with --check-models.

Fix compiler warnings in BV-related code (unused vars mostly).

Fix to the compatibility library (this does fix the build).

Fix compat-Java layer, should fix build.

Lower the Java JRE version requirement.

Adjust library dependencies to be more correct (fixes lintian warnings).

Add some missing functions in configuration and compat library.

Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, and arith.

Minor fixes for man pages.

Some minor cleanup and documentation.

fixed build failure

Implement RecordProperties::mkGroundTerm().  Resolves bug #546.

Bit-vector kinds documentation

fixed merge conflict

added model generation to eager bit-blasting and turned abc off by default

update to abc install instructions

Better --segv-spin messages.

Fix make install-examples.

Proper escaping in option documentation.

Version of the run script that works with trace executor; waiting on StarExec infrastructure for testing.

forgot to add the test with fix

according to bug report, fix was in 6267f3

basic fixes for sets translator, separate binaries

Options script fix.

Fix for mac readline.

Better error for invalid concrete syntax of sorts with too many parens, like (Int).  Thanks to Dan Liew for the report.

Fix GLPK builds: correct access specifier on cut classes.

Java bindings fixes.

Minor Doxygen fixes.

disable unate lemmas when using incremental mode

Fix for pre-C++11 is_sorted().

More minor code cleanup.

No more dependence on libstdc++ or PBDS stuff: remove build stuff that supported it.

New translator features: expand define-funs and combine assertions.

Code cleanup.

Documentation clean-ups.

Another fix for the CASC stuff.

Final preparations for arithmetic for building with libc++.

Fix for new CASC features, fixes Java builds.

Some reversions of recent commits re: portfolio failure.

* Partial reversion of b8e28a7, do it a different way.

* Revert "Test portfolio with --no-wait-to-join."
  This reverts commit 8b56004ee8bf6c34aaf045bec12bf0e4401a044c.

This commit adds a priority queue implementation.  This is to avoid compilation troubles with libc++.

Test portfolio with --no-wait-to-join.

For casc : print models of functions rewritten by sort inference.

Fix rewriter typo.

Clean up glpk detection a little, fix a detection bug.

fix typo

More application-track fixes for use with trace executor.

Versioning preparation.

Some fixes for tear-down-incremental and "success" output.

Disallow context-dependent copy/assignment.

Fix compile errors with some versions of GCC.

Clean up some compiler warnings on 32-bit.

Minor fixes to get-abc script and configure stuff.

get-glpk-cut-log script, and configure code.

dos2unix-convert some sources.

Minor fixes, spelling etc.

More proof support for CASC : include skolemization

minor update to application track config in QF_BV

More doc fixes; fixes some lintian warnings.

Better --segv-spin messages.

Fix make install-examples.

Proper escaping in option documentation.

Version of the run script that works with trace executor; waiting on StarExec infrastructure for testing.

Version of the run script that works with trace executor; waiting on StarExec infrastructure for testing.

Merge remote-tracking branch 'upstream/master' into sets

forgot to add the test with fix

according to bug report, fix was in 6267f3

basic fixes for sets translator, separate binaries

Options script fix.

Fix for mac readline.

Better error for invalid concrete syntax of sorts with too many parens, like (Int).  Thanks to Dan Liew for the report.

Fix GLPK builds: correct access specifier on cut classes.

Java bindings fixes.

Minor Doxygen fixes.

disable unate lemmas when using incremental mode

Some reversions of recent commits re: portfolio failure.

* Partial reversion of b8e28a7, do it a different way.

* Revert "Test portfolio with --no-wait-to-join."
  This reverts commit 8b56004ee8bf6c34aaf045bec12bf0e4401a044c.

Fix for pre-C++11 is_sorted().

More minor code cleanup.

No more dependence on libstdc++ or PBDS stuff: remove build stuff that supported it.

New translator features: expand define-funs and combine assertions.

Merge pull request #33 from mdeters/arith-proposal

Final preparations for arithmetic for building with libc++.

Code cleanup.

Documentation clean-ups.

Another fix for the CASC stuff.

Final preparations for arithmetic for building with libc++.

Fix for new CASC features, fixes Java builds.

Some reversions of recent commits re: portfolio failure.

* Partial reversion of b8e28a7, do it a different way.

* Revert "Test portfolio with --no-wait-to-join."
  This reverts commit 8b56004ee8bf6c34aaf045bec12bf0e4401a044c.

This commit adds a priority queue implementation.  This is to avoid compilation troubles with libc++.

Test portfolio with --no-wait-to-join.

Test portfolio with --no-wait-to-join.

For casc : print models of functions rewritten by sort inference.

Fix rewriter typo.