Minor fixes to build system
Remove PropositionalQuery class and all CUDD-related build stuff (and references)
Fixes for miplib-trick application (and a new testcase)
Minor cleanup of sources
Adding evaluation of constant terms to the equality engine. Evaluation on a particular kind can be set by setting interpreted = true when calling addFunctionKind.
Some statistics for narrowing down incrementality issues (push/pop vs solve timing)
Properly |quote| symbols in SMT-LIBv2 output.
Interactive mode support for multiline input
Remove unintentionally-committed-to-master README from interactive branch
Fix to bug 497: make justification heuristic's ITE cache context-dependent.
Better reporting of detached git state in --version and --show-config
fixing constant evaluation bugs
Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException
more equality constant evaluation
Some model and printing fixes for defined functions in input.
Merge branch 'master' of github.com:CVC4/CVC4
fixing markings of internal nodes in equality engine
Add the ability to "mute" commands, needed for SMT-LIB compliance.
Better error in case of nonlinear assertions while in linear logic
another typo/bugfix for equality constant evaluation