When printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary.

Add operator support (resolves bug #563).

SmtEngine::checkModel() now checks that model values are of the correct type (related to bug #569).

Update commit # for get-abc script, anticipating Liana's merge.

Fix usability issue with tear-down incremental mode.

SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, bvor, and bvxor.

Fixing run-script for smt-comp

Another check when making SMT-COMP submission zipfiles.

Fix StarExec description files for new requirements.

Support E-matching/QCF for Set operators.

Fix for Windows builds (rlimit doesn't exist on Windows).

More make rules

One final bit (I hope) of make magic

More make rules

Bug fix for string-opt2 (copied from Tianyi's branch).

Update submission make rules.

Change SMT COMP script to use external timeouts.

Run script updates: no --stats, also application-track version.

run script fix

Improve --dt-stc-ind for multi-variable datatype properties.

Fixes for --inst-max-level

Fix personal.mk for some make targets.

Minor changes to script.  Disable cbqi sat.

Add option to avoid dumping partial models/proofs.

Some fixes to GC order in Java.

Merge pull request #27 from kbansal/statistics

update stats_black

update stats_black

New --tear-down-incremental mode, useful for debugging and performance profiling.

fix timespec printing

sorry prvs fix added some unrelated code

Revert "timespec printing bug"

This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.

timespec printing bug

Fix typo in Java destruction code; should fix some recent bug reports of crashes in Java.

Improved type-checking for tuple and record selects.

Fix bug 567

This bug got introduced in 96eccb0d6134ccf4ead0134299b2e3750a890083.
The backing Node didn't always exist because of the changes.

Fixing Tim's subtype/solving bug for arrays

Separating an implicit inclusion of smt_engine.h from theory.h.

Fixing a soundness bug due to the default implmentation of Theory::ppAssert() not respecting subtyping.

Improve quantifier instantiation: always use original terms when matching (was missing for simple triggers).   Minor updates to scripts.

Some cleanup, fix warnings raised by Debian packager.

Fix bug in E-matching Real/Int terms.

Safer swig-wrapping for unsigned long long in Java, which will throw an exception if the argument is out of bounds for unsigned long long.  Thanks to Steve Siegel for the report.

Fix compiler warning (missing virtual dtor)

More documentation fixes. Apologies for multiple commits.

Fixing documentation for glpk configuration.

minor fix for string equality engine assertion.

Merge pull request #26 from kbansal/sets

Sets

lfsc_checker: fix some warnings reported by _both_ gcc and clang

sets: fix a bug in model building, another in handling set of sets

minor improvements (fixes) to did-you-mean suggestions

Minor fixes.  Add SMTCOMP 2014 script.

Finish --dump-instantiations option.  Update scripts.

Reject native extended ASCII characters. It requires user to use escaped sequence for an extended ASCII character.

Reject un-escaped extended ASCII characters

Add lazy strategy for bounded integers to avoid non-terminating unsat cases.  Add regressions.

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

Fix a bug in the IndexOf function.

Fix a bug in the IndexOf function.

Minor updates/fix to --cbqi-recurse

Merge remote-tracking branch 'timothy-king/master'

Merging in additional glpk options and statistics from CAV submission.

Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report.

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

Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.

Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.

More preparation for CASC proofs.  Minor fix for sort inference (rewrite new assertions).  Bug fix for ambqi : simplify correctly for multi-sorted case.  Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.

Bug fixes to CBQI.  Add first draft of CASC j7 TFF script.  Add regression, minor changes.

Fix for example installation.

Initial draft of run scripts for CASC j7

Add variable ordering to ambqi.  Bug fix to macros. More preparation for CASC proofs.

Major simplifications to macros module.

Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers.  Minor fixes to ambqi.  Preparation for CASC proof output.  Add NNF option.

Basic optimizations for ambqi : only normalize UF applied to variables, direct handling of NOT

Adding encoding of sha1 collision for the hashing example

patch to the last commit: add a single character case

fix a bug in contain

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

add splits

add splits

Fixes to ambqi, now solution-sound.

First draft of ambqi_builder (new implementation of MBQI based on disjoint sets).

fix a bug in replace and contains

add constant regular expression check for intersection.

Improving documentation for glpk-cut-log switch.

Valuation::entailmentCheck() proxy for TheoryEngine version.  Signature and contract is the same as for TheoryEngine version.

Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.

Simplification of EqualityEngine::areDisequal.  Comparison for production : church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5.  Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.

Fix assertion from previous commit.

Add option --dt-stc-ind for strengthening skolemization.  Refactor skolemization.

More minor optimizations for datatypes.

Minor optimizations to datatypes, revert to checkClash not mod eq.  Minor clean up.

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

decision engine: cache start index for and/or nodes

This is done only in "hard" case. Limited testing has not shown
improvement in the "easy" case.

This was triggerred by a benchmark sent by andy/viktor.

performance comparison notes for the change on wiki
http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex

T-entailment work, and QCF (quant conflict find) work that uses it.

This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

Fix warnings, cleanup in strings typechecker.

Fix compiler warning re: TheoryUF destructor.

Fix simplify output for SMT2 printer.

Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrite-divk.

Mostly resolves bug #561 memory leaks, and more.

Fix for --force-logic to extend its reach to the parser.

fixed couple of more warnings