cvc5.git
2013-05-22 Andrew ReynoldsAdd regressions for finite model finding
2013-05-21 Morgan DetersMerge branch '1.2.x'
2013-05-21 Morgan DetersFix bug 512: an assertion failure only appearing with...
2013-05-21 Morgan DetersFix an error that valgrind found.
2013-05-21 Morgan DetersMerge branch '1.2.x'
2013-05-21 Morgan DetersFix incremental bug in symmetry breaker.
2013-05-20 Morgan DetersMerge branch '1.2.x'
2013-05-20 Morgan DetersFix error reporting on use of (nonlinear) div,mod,...
2013-05-20 Morgan DetersUpdate THANKS to mention David Cok's contributions.
2013-05-20 Morgan DetersDetect multiply-defined :named annotations and issue...
2013-05-20 Morgan DetersFix parsing of SMT-LIBv2 |quoted| symbols that span...
2013-05-20 Morgan DetersCompliance fixes for :named annotations: they must...
2013-05-20 Morgan DetersDon't allow get-model & co after a user push/pop
2013-05-20 Morgan DetersAs per SMT-LIB standard: make - and xor take n>2 args...
2013-05-20 Morgan DetersFix for equality-chaining of Booleans in SMT-LIBv2.
2013-05-20 Morgan DetersFix destruction issue in GetValueCommand leading to...
2013-05-20 Morgan DetersBetter error on invalid logic strings.
2013-05-20 Morgan DetersBetter error on illegal (pop N); also more compliant...
2013-05-20 Morgan DetersA couple of fixes to the get-option command for complia...
2013-05-20 Morgan DetersDisallow construction of (_ BitVec 0).
2013-05-20 Morgan DetersFixed "success" response to (push N) / (pop N) with...
2013-05-20 Morgan DetersFix to empty response to (get-assignment).
2013-05-20 Morgan Detersconfigure fix for building with glpk on redhat, perhaps...
2013-05-20 Morgan Detersminor changes to language bindings
2013-05-20 Morgan Detersdisable Logic-checking with finite model finding for...
2013-05-20 Morgan DetersFix erroneous results when the logic was incorrectly...
2013-05-20 Andrew ReynoldsPossible final version of run scripts for casc.
2013-05-17 Andrew ReynoldsAdd model-producing run script for casc.
2013-05-17 Andrew ReynoldsAdd support for --dump-models option, in preparation...
2013-05-17 Morgan DetersAs per SMT-LIB standard: make - and xor take n>2 args...
2013-05-17 Morgan DetersFix for equality-chaining of Booleans in SMT-LIBv2.
2013-05-17 Morgan DetersFix destruction issue in GetValueCommand leading to...
2013-05-17 Morgan DetersBetter error on invalid logic strings.
2013-05-17 Morgan DetersBetter error on illegal (pop N); also more compliant...
2013-05-17 Morgan DetersA couple of fixes to the get-option command for complia...
2013-05-17 Morgan DetersDisallow construction of (_ BitVec 0).
2013-05-17 Morgan DetersFixed "success" response to (push N) / (pop N) with...
2013-05-17 Morgan DetersFix to empty response to (get-assignment).
2013-05-16 Morgan Detersconfigure fix for building with glpk on redhat, perhaps...
2013-05-16 Andrew ReynoldsFix minor bug in full_model_check.cpp
2013-05-16 Morgan Detersminor changes to language bindings
2013-05-14 Andrew ReynoldsUpdate casc24-fnt run script. Add casc24-fof run script.
2013-05-14 lianahadded some extra options to the bit-vector theory
2013-05-14 Andrew ReynoldsAdd support for quantifier patterns in smt2 printer.
2013-05-14 Andrew ReynoldsRefactoring to separate old and new model building...
2013-05-11 Andrew ReynoldsPreliminary version of finite model finding over bounde...
2013-05-10 Morgan Detersdisable Logic-checking with finite model finding for...
2013-05-10 lianahnow proofs print mapping between atom and propositional...
2013-05-10 Andrew ReynoldsUpdate casc run script. Work on compliance for SZS...
2013-05-10 lianahfixes to the proof system so it works with theory lemma...
2013-05-10 Morgan DetersFix erroneous results when the logic was incorrectly...
2013-05-10 Morgan DetersAdd documentation for --disable-fmf-inst-gen, which...
2013-05-10 Andrew ReynoldsAdd simplification option --fo-prop-quant. Add model...
2013-05-09 Kshitij BansalMerge branch 'master' of ssh://github.com/CVC4/CVC4
2013-05-09 Tim KingChanging the integer normal form to increase matching.
2013-05-09 Andrew ReynoldsAdd new method for checking candidate models, --fmf...
2013-05-08 Kshitij Bansalrm decision/relevancy
2013-05-08 Morgan DetersPrerelease versioning for 1.2.x
2013-05-08 Morgan DetersPrerelease versioning for master
2013-05-08 Morgan DetersMerge tag 'smteval2013'
2013-05-08 Morgan DetersCutting release 1.2.
2013-05-08 Morgan DetersRemoving arithmetic compile warning for release
2013-05-08 Morgan Detersupdate versioning
2013-05-08 Morgan Detersfinal updates for smt-eval script
2013-05-08 Clark BarrettFixed assertion bug
2013-05-08 Morgan Detersfix for smt-eval run script
2013-05-07 Morgan DetersBV strategy for SMT-EVAL
2013-05-07 Morgan Detersfix for nonterminating model-based array loop
2013-05-07 lianahadded type checking rule to check for bit-vector consta...
2013-05-07 lianahone more fix for rewrites
2013-05-07 lianahfixed bv rewrite blow-up
2013-05-07 Dejan Jovanovićfix for bug500
2013-05-07 Tim KingFixes a bug with arithmetic's new attempt solution...
2013-05-07 Tim KingImproving arithmetic debugging output.
2013-05-07 Tim KingDisabling an incorrect prototyping line from the simple...
2013-05-07 Morgan DetersChange SMT-EVAL run-script to use Tim's best QF_LRA...
2013-05-07 Liana Hadareanfixed bv rewrite rule bug
2013-05-06 Morgan DetersRemoving excess verbosity from ApproxSimplex (after...
2013-05-06 Tim KingAdding a heuristic for guessing an optimization functio...
2013-05-06 Tim KingDisables justification stop only for LRA if the problem...
2013-05-06 Clark BarrettSome bug fixes for mb arrays
2013-05-05 Tim KingAdding cut offs for likely integer infeasible paths.
2013-05-04 Tim KingAdding a smarter technique for pivoting in solutions...
2013-05-03 Tim KingFixing compilation of unit tests. These problems were...
2013-05-03 Tim KingMore misc. arithmetic cleanup. Removing unused files...
2013-05-03 Tim KingCode cleanup. Reducing misc. warnings in arithmetic.
2013-05-03 Tim KingRemoving arithmetic legacy code and unifying functions.
2013-05-03 Tim KingFixing a debug typo.
2013-05-03 Tim KingMerging branch 'soiquickexplain'.
2013-05-03 Tim KingMerge branch 'fcexplanations'
2013-05-02 Tim KingAdding quick explain for soi simplex.
2013-05-02 Dejan Jovanović* splitLemma to request atoms
2013-05-02 lianahmerged master
2013-05-02 lianahMerge branch 'master' of https://github.com/CVC4/CVC4
2013-05-01 Morgan DetersComment out some debug-related things in attribute...
2013-05-01 Morgan DetersFix to dumping re: boolean terms, datatypes
2013-05-01 Morgan DetersFix to boolean-terms; resolves bug #507
2013-05-01 lianahremoved tracing code causing slowdown; cleaned up some...
2013-05-01 Tim KingWorking on the new explanation system.
2013-05-01 lianahadded back BitwiseEq rule
next