projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
add bag.fold operator (#7718)
[cvc5.git] / test / regress / regress0 /
2021-12-02 Gereon KremerAdd unit tests for api::Solver::setOption() (#7708) tree | commitdiff
2021-12-01 Andrew ReynoldsRemove spurious assertion in parser (#7713) tree | commitdiff
2021-11-30 Andrew ReynoldsProper check for first-class types in datatype subfield... tree | commitdiff
2021-11-30 Gereon KremerRemove now unused dumping infrastructure (#7703) tree | commitdiff
2021-11-25 Mathias PreinerGuard regression tests that require libpoly to pass... tree | commitdiff
2021-11-17 Andres NoetzliFix binding of quoted symbols in `define-fun` (#7655) tree | commitdiff
2021-11-16 Haniel Barbosa[proofs] Make sure --proof-check=... is no-op when... tree | commitdiff
2021-11-13 Andres NoetzliSkip `str.code` inferences for sequence eqcs (#7644) tree | commitdiff
2021-11-11 Andrew ReynoldsAdd lazy approach for handling lambdas in the HO extens... tree | commitdiff
2021-11-10 Andrew ReynoldsFix parsing array constants (#7617) tree | commitdiff
2021-11-10 Aina Niemetzsets: Rename set.intersection to set.inter. (#7622) tree | commitdiff
2021-11-09 Gereon KremerRemove command-verbosity option (#7581) tree | commitdiff
2021-11-08 Aina Niemetzsets: Rename kinds with a more consistent naming scheme... tree | commitdiff
2021-11-06 Abdalrhman MohamedPrint `unsupported` for unrecognized flags. (#7384) tree | commitdiff
2021-11-05 Haniel Barbosa[proofs] Fix open sat proof (#7509) tree | commitdiff
2021-11-05 Andres Noetzli[FP] Do not assert that model has shared term (#7585) tree | commitdiff
2021-11-05 Gereon KremerRemove quadratic solving in NlModel (#7542) tree | commitdiff
2021-11-04 Andrew ReynoldsAdd -o sygus-grammar to print auto-generated SyGuS... tree | commitdiff
2021-11-04 Andrew ReynoldsReplace the old dump infrastructure (#7572) tree | commitdiff
2021-11-04 Gereon KremerStart refactoring of `-o` and `-v` (#7449) tree | commitdiff
2021-11-03 Andrew ReynoldsFix preregistration for floating point theory (#7558) tree | commitdiff
2021-11-02 Andrew ReynoldsImprove syntax for fmf cardinality constraints (#7556) tree | commitdiff
2021-11-01 Mathias Preinerbv: Remove layered solver. (#7455) tree | commitdiff
2021-10-29 Gereon KremerFix proof of nl lemma for a corner case (#7530) tree | commitdiff
2021-10-29 Andrew ReynoldsFix model construction for higher order involving irrel... tree | commitdiff
2021-10-28 Gereon KremerFix proof for xor in circuit propagator (#7525) tree | commitdiff
2021-10-28 Haniel Barbosa[proofs] Fix assertion in EqProof conversion (#7522) tree | commitdiff
2021-10-28 Abdalrhman MohamedAdd a `define-fun` command for each `:named` term.... tree | commitdiff
2021-10-28 Abdalrhman MohamedFix `(set-info <sexpr>)` parsing and printing bugs... tree | commitdiff
2021-10-27 Andrew ReynoldsAdd missing API checks to getValue (#7475) tree | commitdiff
2021-10-27 Andres NoetzliRequire ITE branches to be first class types (#7508) tree | commitdiff
2021-10-27 Andrew ReynoldsFix care graph computation for higher-order (#7474) tree | commitdiff
2021-10-27 Andrew ReynoldsFix model unsoundness for relation join (#7511) tree | commitdiff
2021-10-27 Gereon KremerMake --version exit (#7506) tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Fix singleton check in MACRO_RES post-processi... tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Reset local var in SatProofManager since incre... tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Fix and simplify CHAIN_RESOLUTION checker... tree | commitdiff
2021-10-26 Andrew ReynoldsAdd regressions for fixed issues (#7495) tree | commitdiff
2021-10-25 Andrew ReynoldsFix support for global declarations (#7480) tree | commitdiff
2021-10-22 Haniel Barbosa[proof] Fixing CHAIN_RESOLUTION checker (#7465) tree | commitdiff
2021-10-22 Gereon KremerFix another double negation proof issue (#7468) tree | commitdiff
2021-10-22 Gereon KremerMake CAD proofs user context dependent (#7466) tree | commitdiff
2021-10-21 Gereon KremerAlso fix case of negated ite (#7454) tree | commitdiff
2021-10-21 Gereon KremerFix symmetric proof issue for ITE in circuit propagator... tree | commitdiff
2021-10-21 Haniel Barbosa[proofs] Fix open proof in SAT solver due to cycles... tree | commitdiff
2021-10-21 Gereon KremerAdd regression (#7447) tree | commitdiff
2021-10-21 Gereon KremerFix incorrect proof from ITE in circuit propagator... tree | commitdiff
2021-10-21 Andres NoetzliEnable and fix dump test (#7387) tree | commitdiff
2021-10-21 Gereon KremerFix (#7437) tree | commitdiff
2021-10-20 Andrew ReynoldsReimplement support for relational triggers (#7063) tree | commitdiff
2021-10-20 Andrew ReynoldsCorrectly parse uninterpreted constant values in get... tree | commitdiff
2021-10-18 Abdalrhman MohamedMove check for experimental arrays features to `theory_... tree | commitdiff
2021-10-15 Andrew ReynoldsAdd more regressions for fixed issues (#7382) tree | commitdiff
2021-10-14 Andrew ReynoldsAdd regressions for fixed issues (#7369) tree | commitdiff
2021-10-14 Gereon KremerImprove ManagedStreams (#7367) tree | commitdiff
2021-10-14 Andrew ReynoldsFix quantifiers variable elimination for parametric... tree | commitdiff
2021-10-11 Andrew ReynoldsConnect the LFSC printer (#7323) tree | commitdiff
2021-10-06 Gereon KremerChange semantics of dumpUnsatCoresFull (#7314) tree | commitdiff
2021-10-01 Andrew ReynoldsFix ascription check for return types on ordinary funct... tree | commitdiff
2021-09-30 Andrew ReynoldsSimplify the syntax and representation of the separatio... tree | commitdiff
2021-09-29 Abdalrhman MohamedRemove support for extended `(check-sat <term>)` comman... tree | commitdiff
2021-09-29 Andrew ReynoldsUpdate the syntax for tuples in smt2 (#7265) tree | commitdiff
2021-09-22 Mathias PreinerRemove CVC language support (#7219) tree | commitdiff
2021-09-22 Andrew ReynoldsMinimal fixing version for tuple update parsing (#7228) tree | commitdiff
2021-09-14 Andrew ReynoldsSupport sygus version 2.1 command assume (#7081) tree | commitdiff
2021-09-14 Mathias Preinerproofs: Properly track pre- and post-rewrites in bbAtom... tree | commitdiff
2021-09-14 Andrew ReynoldsReimplement `--dump=raw-benchmark` as `-o raw-benchmark... tree | commitdiff
2021-09-11 Mathias Preinerbv: Move IsPowerOfTwo rule to preprocessing pass and... tree | commitdiff
2021-09-10 Aina NiemetzFP: Do not send trivial lemmas. (#7167) tree | commitdiff
2021-09-07 Andrew ReynoldsRefactoring and fixes of set defaults for quantifiers... tree | commitdiff
2021-09-02 Andrew ReynoldsImplement lazy proof checking modes (#7106) tree | commitdiff
2021-09-02 Aina NiemetzEnable sygus-inst for FP, NIA and NRA. (#7098) tree | commitdiff
2021-09-01 Andrew ReynoldsPrint response to get-model using the API (#7084) tree | commitdiff
2021-08-30 Andrew ReynoldsFix quantifiers dynamic split module for parametric... tree | commitdiff
2021-08-26 Mathias Preinerint2bv: Fix conversion of signed bit-vector values... tree | commitdiff
2021-08-26 Gereon KremerConsolidate language types (#7065) tree | commitdiff
2021-08-23 Andrew ReynoldsPurify substitutions in strings proof reconstruction... tree | commitdiff
2021-08-23 Andrew ReynoldsGeneralize inequality elimination in quantifiers rewrit... tree | commitdiff
2021-08-23 Andrew ReynoldsFix single invocation partition for higher-order (... tree | commitdiff
2021-08-20 Andrew ReynoldsSupport sygus standard command syntax set-feature ... tree | commitdiff
2021-08-18 Andres NoetzliMinor fixes of policy for eliminating quantifiers ... tree | commitdiff
2021-08-17 Andrew ReynoldsFix policy for eliminating quantified formulas (#7017) tree | commitdiff
2021-08-09 Andrew V. JonesCreate grouping of tests that exercise '--use-approx... tree | commitdiff
2021-07-30 Gereon KremerAllow changing certain options while solving (#6945) tree | commitdiff
2021-07-29 Haniel Barbosa[proofs] Set BV solver to better proof-producing one... tree | commitdiff
2021-07-29 Andrew ReynoldsIntegrate central equality engine approach into theory... tree | commitdiff
2021-07-23 Aina NiemetzFP: Add option to word-blast more lazily. (#6904) tree | commitdiff
2021-07-15 Mathias Preinerbv: Rename simple solver to bitblast-internal. (#6888) tree | commitdiff
2021-07-14 Haniel Barbosa[proof] Fix open proof issues in SAT proof (#6887) tree | commitdiff
2021-07-14 Haniel BarbosaAdd option that exercises the previously buggy behavior... tree | commitdiff
2021-07-14 Andrew ReynoldsFix for context on input proof generator (#6873) tree | commitdiff
2021-07-14 Gereon KremerClean up option usage in command executor (#6844) tree | commitdiff
2021-07-13 Haniel Barbosa[rewriter] Add rewrite to order IFF (equality for Boole... tree | commitdiff
2021-07-09 Haniel Barbosatest also with default cores (#6858) tree | commitdiff
2021-07-09 Andres NoetzliMake regression test `issue4971-0` more robust (#6857) tree | commitdiff
2021-07-07 Haniel Barbosa[unsat cores] Adding regressions from #4971 (#6852) tree | commitdiff
2021-07-07 Aina NiemetzRename operator pow2 to int.pow2. (#6849) tree | commitdiff
2021-07-07 Andrew ReynoldsFix regressions for competition build (#6846) tree | commitdiff
2021-07-05 Andres Noetzli[Strings] Fix incorrect rewrite (#6837) tree | commitdiff
2021-07-03 Mathias PreinerAdd output tags -o, --output. (#6826) tree | commitdiff
next