Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-12-06 | Enable BV proofs when using an eager bitblaster (#2733) | Alex Ozdemir | |
* Enable BV proofs when using and eager bitblaster Specifically: * Removed assertions that blocked them. * Made sure that only bitvectors were stored in the BV const let-map * Prevented true/false from being bit-blasted by the eager bitblaster Also: * uncommented "no-check-proofs" from relevant tests * Option handler logic for BV proofs BV eager proofs only work when minisat is the sat solver being used by the BV theory. Added logic to the --proof hanlder to verify this or throw an option exception. * Bugfix for proof options handler I forgot that proofEnabledBuild runs even if the --proof option is negated. In my handler I now check that proofs are enabled. * Clang-format | |||
2018-09-22 | cmake: Added regression tests and target make regress. | Aina Niemetz | |
2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
2018-08-01 | Fix issues with bv2nat (#2219) | Andrew Reynolds | |
This includes: - A missing case in the smt2 printer, - A bug in an inference of int2bv applied to bv2nat where the types are different. | |||
2018-07-21 | Remove --no-check-proofs and --no-check-unsat-cores from a satisfiable test ↵ | yoni206 | |
(#2184) | |||
2018-05-08 | Refactor bv-abstraction preprocessing pass. (#1860) | Mathias Preiner | |
2018-03-21 | Move regression tests to single Makefile.am (#1658) | Andres Noetzli | |
Until now, regression tests were split across tens of different Makefile.am, which required a lot of code duplication and does not really seem to be in the spirit of automake. If we want to change the LOG_COMPILER/LOG_DRIVER for example, we have to change every single Makefile.am, which is cumbersome (I was able to get something semi-working by exporting those variables but it didn't seem very clean). Additionally, it made the output of the regression tests fairly verbose and split the output across multiple log files. Finally it also limited parallelism when running the regression tests (this fix lowers the time it takes to run regression level 1 from 3m to 1m45s on my machine with 16 threads). This commit moves all the regression tests into test/regress/Makefile.tests and changes test/regress/Makefile.am to deal with this new structure. Finally, it changes how the test summary in test/Makefile.am is produced: instead of relying on the log files for the subdirectories, it greps for the test results in the log files of the individual tests. Not the most elegant solution but we should probably anyway delegate that task to a Python script at some point. | |||
2018-02-15 | Refactor regressions (#1581) | Andrew Reynolds | |
2016-10-21 | Fix/add missing makefiles. | ajreynol | |
2016-10-21 | Move slow regress0 benchmarks to regress1, increment regress1 through regress3. | ajreynol | |