Permalink
Commits on Dec 20, 2012
  1. Committing a light version of the testsuite that does

    not contain any CF contracts, in order to experiment
    completeness and finite models without the CF-related
    complications. The examples are taken from new-testsuite/
    
    There is already an interesting finding: the append contracts
    hold (and 'minrec' is able to say UNSAT), but they appear to
    be non-provable (SAT) in master branch. I don't really know
    what to say, but there must be something incomplete in master.
    
    NB: 'minrec' vs 'min' does not play a role here -- minrec only
    has to do with CF and there are no CF contracts in this testsuite.
    dimitriv committed Dec 20, 2012
Commits on Nov 1, 2012
Commits on Oct 31, 2012
  1. Fix so contracts still compiles with 7.4.1

    Dan Rosén committed Oct 31, 2012
Commits on Oct 23, 2012
  1. TPTP is no longer supported in Z3 (since v.4.1)

    Artem Glebov committed Oct 23, 2012
  2. Using SMT2.0 for Z3 - SMT1.5 no longer supported

    Artem Glebov committed Oct 23, 2012
Commits on Oct 17, 2012
Commits on Oct 16, 2012
Commits on Sep 27, 2012
  1. Add some suggestions on failure

    Dan Rosén committed Sep 27, 2012
  2. More informative error message.

    dimitriv committed Sep 27, 2012
Commits on Sep 7, 2012
  1. Update testsuite

    Dan Rosén committed Sep 7, 2012
Commits on Sep 6, 2012
Commits on Sep 4, 2012
  1. Rename Contracts modules and related parameters

    Dan Rosén committed Sep 4, 2012
  2. Restructure directories

    Dan Rosén committed Sep 4, 2012
  3. Add two incoming examples with Int, mc91 and DataMap

    Dan Rosén committed Sep 4, 2012
  4. Describe pairs with SMT data type declaration

    Dan Rosén committed Sep 4, 2012
Commits on Sep 3, 2012
Commits on Aug 31, 2012
  1. Wibbles to test suite runner

    Dan Rosén committed Aug 31, 2012
  2. Wibbles to test suite

    Dan Rosén committed Aug 31, 2012
  3. Add SMT support for Int

    Dan Rosén committed Aug 31, 2012
  4. Add result summaries from timing the test suite

    Dan Rosén committed Aug 31, 2012
Commits on Aug 30, 2012
  1. Add SMT Lineariser

    Dan Rosén committed Aug 30, 2012
  2. Add crash free pairs smt, tptp and mail

    Dan Rosén committed Aug 30, 2012
  3. Update runner so csv timings can be output

    Dan Rosén committed Aug 30, 2012
  4. Be a bit more quiet about what files are produced

    Dan Rosén committed Aug 30, 2012
  5. Time how long time proving takes

    Also remove the shqq dependency
    Dan Rosén committed Aug 30, 2012
  6. Remove min guard from --all-disjoint

    Dan Rosén committed Aug 30, 2012
Commits on Aug 28, 2012
  1. Update MapFromJust; cannot countersatisfy the helpers

    Dan Rosén committed Aug 28, 2012
  2. Add a little test about tcMatchTy and tcUnifyTys

    Dan Rosén committed Aug 28, 2012
Commits on Aug 27, 2012
  1. Simplify the implementation of CF axioms

    Dan Rosén committed Aug 27, 2012
  2. Add fancy ascii logo

    Dan Rosén committed Aug 27, 2012