summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2018-10-18Non-implied mode for model cores (#2653)Andrew Reynolds
2018-10-18Non-contributing find replace rewrite (#2652)Andrew Reynolds
2018-10-05Update default options for sygus (#2586)Andrew Reynolds
2018-10-02Allow (_ to_fp ...) in strict parsing mode (#2566)Andres Noetzli
2018-09-30Add rewrite for solving stoi (#2532)Andrew Reynolds
2018-09-26 Fix homogeneous string constant rewrite (#2545)Andrew Reynolds
2018-09-26Makes SyGuS parsing more robust in invariant problems (#2509)Haniel Barbosa
2018-09-24Fix quantifiers selector over store rewrite (#2510)Andrew Reynolds
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-11Support model cores via option --produce-model-cores. (#2407)Andrew Reynolds
2018-09-06Refactor and document quantifiers variable elimination and conditional splitt...Andrew Reynolds
2018-09-05 Extended rewriter for string equalities (#2427)Andrew Reynolds
2018-09-04Make quantifiers strategies exit immediately when in conflict (#2099)Andrew Reynolds
2018-08-30Add regular expression elimination module (#2400)Andrew Reynolds
2018-08-28Fix sort inference for quantified variables of interpreted types (#2393)Andrew Reynolds
2018-08-27Refactor extended rewriter, move rewrites to aggressive (#2387)Andrew Reynolds
2018-08-27Make division chainable in the smt2 parser (#2367)Andrew Reynolds
2018-08-24Refactor nlExtPurify preprocessing pass (#1963)Haniel Barbosa
2018-08-22Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253)yoni206
2018-08-22Adds regression test for automatic generation of SyGuS BV grammars (#2345)Haniel Barbosa
2018-08-21Makes the new row propagation system default (#2335)Haniel Barbosa
2018-08-20Remove support for *.expect files in regressions (#2341)Andres Noetzli
2018-08-20Add regressions that increase coverage (#2337)Andrew Reynolds
2018-08-17 Fix spurious warning in sort inference (#2331)Andrew Reynolds
2018-08-16Refactor extended rewriter preprocessing pass (#2324)Haniel Barbosa
2018-08-16Refactor apply2const (#2316)Haniel Barbosa
2018-08-15Make sort inference a preprocessing pass (#2309)Andrew Reynolds
2018-08-13Fix get-unsat-assumptions output (#2301)Andres Noetzli
2018-08-07Fix inference of pre and post conditions for non variable arguments. (#2237)Andrew Reynolds
2018-08-02Parse standard separation logic inputs (#2257)Andrew Reynolds
2018-07-30Add support for incremental eager bit-blasting. (#1838)Mathias Preiner
2018-07-26Disabling bvLazyRewriteExtf in the right place (#2214)yoni206
2018-07-23 sygusComp2018: add regressions (#2191)Andrew Reynolds
2018-07-17Refactor sep-pre-skolem-emp preprocessing passyoni206
2018-07-13Properly clean up assertion stack in CnfProof (#2147)Andres Noetzli
2018-07-13 sygusComp2018: optimization for collect model info (#2105)Andrew Reynolds
2018-07-02Add regression test for issue #1986 (#2114)Andres Noetzli
2018-06-12Fix strip constant endpoint for ITOS in strings rewriter (#2067)Andrew Reynolds
2018-06-08Reset decisions at SAT level after solving (#2059)Andres Noetzli
2018-06-04Only enable transcendentals if logic is N[I]RAT (#2052)Andres Noetzli
2018-06-04Regressions: Support for requiring CVC4 features (#2044)Andres Noetzli
2018-06-02Fix BV-abstraction check to consider SKOLEM. (#2042)Mathias Preiner
2018-06-01Fix quantified bv variable elimination (#2039)Andrew Reynolds
2018-06-01 Use monomial sum utility to solve for quantifiers macros (#2038)Andrew Reynolds
2018-05-30Fix bv-abstraction check for AND with non bit-vector atoms. (#2024)Mathias Preiner
2018-05-29 Make user's SMT2 version override file version (#2004)Andres Noetzli
2018-05-25Reenable repair const (#1983)Andrew Reynolds
2018-05-22Set same options for proofs as for unsat cores (#1957)Andres Noetzli
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback