projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix exact sqrt (#3721)
[cvc5.git] / test / regress / regress0 /
2020-02-07 Andrew ReynoldsFix exact sqrt (#3721) tree | commitdiff
2020-02-04 Alex OzdemirRegression tests for arithmetic proofs. (#3701) tree | commitdiff
2020-02-03 Andrew ReynoldsMinor fixes to regressions (#3702) tree | commitdiff
2020-02-03 Andrew ReynoldsFix invariant template inference for trivially infeasib... tree | commitdiff
2020-01-31 Andres NoetzliFix arithmetic rewriter for exponential (#3688) tree | commitdiff
2020-01-30 Andrew ReynoldsEnsure literals in FMF decision strategies are in the... tree | commitdiff
2020-01-30 Andrew ReynoldsDo not debug check model for models with approximations... tree | commitdiff
2020-01-29 Andrew ReynoldsFix isLeq function in String utility (#3659) tree | commitdiff
2020-01-28 Andrew ReynoldsAvoid PLUS with one child for bv2nat elimination (... tree | commitdiff
2020-01-22 Andrew ReynoldsFix parameteric sorts involving Booleans in sygus defau... tree | commitdiff
2020-01-10 Andres NoetzliFix printing of models of uninterpreted sorts (#3597) tree | commitdiff
2019-12-31 Alex Ozdemir[proof] ITE translation fix (#3484) tree | commitdiff
2019-12-23 Andrew ReynoldsInitial support for string reverse (#3581) tree | commitdiff
2019-12-18 Andres NoetzliAvoid calling rewriter from type checker (#3548) tree | commitdiff
2019-12-17 Andrew ReynoldsFix spurious parse error for rational real array consta... tree | commitdiff
2019-12-16 Ying ShengSupport ackermannization on uninterpreted sorts in... tree | commitdiff
2019-12-13 Andrew ReynoldsAdd support for set comprehension (#3312) tree | commitdiff
2019-12-10 Haniel BarbosaFix ufho issues (#3551) tree | commitdiff
2019-12-05 Andrew ReynoldsMake nonlinear solver intercept model assignments from... tree | commitdiff
2019-12-05 Andrew ReynoldsRefactor mode options for Unif+PI (#3531) tree | commitdiff
2019-12-05 Andres NoetzliBi-directional unrolling of R* regular expressions... tree | commitdiff
2019-12-05 Andrew ReynoldsFix the subtyping relation for functions (#3494) tree | commitdiff
2019-12-02 Andres Noetzli[SMT2 Printer] Quote symbols starting with digit (... tree | commitdiff
2019-12-02 Andrew ReynoldsEnsure quantifiers options are set with --no-strings... tree | commitdiff
2019-11-30 Andres NoetzliCompetition build: Skip parsing error regression (... tree | commitdiff
2019-11-27 Andrew Reynolds Fix indexof range lemma (#3499) tree | commitdiff
2019-11-25 Andrew ReynoldsBetter front-end type checking for SyGuS (#3496) tree | commitdiff
2019-11-19 Andres NoetzliFix reduction of `sqrt` (#3478) tree | commitdiff
2019-11-13 Andres NoetzliAllow (set-logic ...) after (reset) (#3457) tree | commitdiff
2019-11-04 Andrew ReynoldsAvoid non-well-founded sygus grammars (#3434) tree | commitdiff
2019-10-28 Andrew ReynoldsFix for non-linear models (#3410) tree | commitdiff
2019-10-28 Andres NoetzliFix integer division rewrite (#3415) tree | commitdiff
2019-10-27 Andres NoetzliFix global-declarations support (#3403) tree | commitdiff
2019-10-15 Andres NoetzliFix regression (#3393) tree | commitdiff
2019-10-14 Andres NoetzliDisable regression test for competition build (#3388) tree | commitdiff
2019-10-13 Andrew ReynoldsEliminate negative constant coefficients in div/mod... tree | commitdiff
2019-10-11 Andrew ReynoldsCheck that logic is set when synth-fun command is encou... tree | commitdiff
2019-10-09 Andres NoetzliAvoid printing success for `--force-logic` (#3363) tree | commitdiff
2019-10-08 Andrew ReynoldsLimit cases of sygus inference based on type (#3370) tree | commitdiff
2019-10-08 Andres Noetzli[CVC Parser] Add support for regular expressions (... tree | commitdiff
2019-10-08 Andres NoetzliDisallow --proof and --incremental (#3332) tree | commitdiff
2019-10-08 Ying ShengMake ackermannization generally applicable rather than... tree | commitdiff
2019-10-03 yoni206Disable proofs for unsupported logics (#3327) tree | commitdiff
2019-10-01 Andrew ReynoldsTrivial solve method for single invocation sygus (... tree | commitdiff
2019-09-27 Andrew ReynoldsCVC print support for recoverable failure (#3323) tree | commitdiff
2019-09-25 Andrew ReynoldsReturn choice functions for approximate values in get... tree | commitdiff
2019-09-18 Andrew ReynoldsDecouple fmf-bound and finite-model-find (#3297) tree | commitdiff
2019-09-13 Andrew ReynoldsDisallow let in sygus grammars, check for free variable... tree | commitdiff
2019-09-11 Andrew ReynoldsFix constructor type printing (#3246) tree | commitdiff
2019-09-06 Mathias PreinerRemove SMT1 parser. (#3228) tree | commitdiff
2019-09-04 Mathias PreinerRemove duplicate regression tests. (#3227) tree | commitdiff
2019-08-30 Andres NoetzliBetter heuristic for str.code/re.range (#3220) tree | commitdiff
2019-08-30 Andres NoetzliInfer conflicts based on regular expression inclusion... tree | commitdiff
2019-08-13 Andrew ReynoldsProperly implement logic info for separation logic... tree | commitdiff
2019-08-06 Andrew ReynoldsProperly parse qualified identifiers (#3111) tree | commitdiff
2019-08-04 Mathias PreinerFix regression script for incremental SMT-LIB v2 benchm... tree | commitdiff
2019-08-02 Mathias PreinerUpdate CaDiCaL to version 1.0.3. (#3137) tree | commitdiff
2019-08-02 Andrew ReynoldsEnable sygus logic when produce-abducts is true (#3144) tree | commitdiff
2019-07-31 Haniel BarbosaParsing THF and adding several regressions (#3131) tree | commitdiff
2019-07-30 Andrew ReynoldsMinor improvement for rewriter for str.replace (#3124) tree | commitdiff
2019-07-30 Haniel BarbosaRemove hard coded option for TPTP regressions in run_re... tree | commitdiff
2019-07-23 Andrew ReynoldsFix sygus datatype parsing in sygus v1 format (#3113) tree | commitdiff
2019-07-18 Andrew ReynoldsBasic rewrites for tolower/toupper (#3095) tree | commitdiff
2019-07-16 Andrew ReynoldsAdd support for str.tolower and str.toupper (#3092) tree | commitdiff
2019-06-21 Andres NoetzliFix and simplify handling of --force-logic (#3062) tree | commitdiff
2019-06-12 Andres NoetzliRefactor parser to define fewer tokens for symbols... tree | commitdiff
2019-06-12 Andres NoetzliDisable dumping regression for non-dumping builds ... tree | commitdiff
2019-06-05 Andres NoetzliPrevent letification from shadowing variables (#3042) tree | commitdiff
2019-06-04 Andres NoetzliEnable proof checking for QF_LRA benchmarks (#2928) tree | commitdiff
2019-06-04 Andres NoetzliAdd check that result matches benchmark status (#3028) tree | commitdiff
2019-05-30 Andres NoetzliQuote symbol when printing empty symbol name (#3025) tree | commitdiff
2019-05-27 Andres NoetzliAvoid substituting Boolean term variables (#3022) tree | commitdiff
2019-05-21 MartinUpdate to symfpu 0.0.7, fixes RTI 3/5 issue (#3007) tree | commitdiff
2019-05-18 Aina NiemetzFP: Fix regression test and enable SymFPU on Travis... tree | commitdiff
2019-05-17 MartinAdd the problematic input from issue 2183 as a regressi... tree | commitdiff
2019-05-15 Andres NoetzliFix model of Boolean vars with eager bit-blaster (... tree | commitdiff
2019-05-06 Andres NoetzliAdd support for re.all (#2980) tree | commitdiff
2019-04-30 Andrew ReynoldsRemove stoi solve rewrite (#2985) tree | commitdiff
2019-04-30 Andrew ReynoldsEliminate APPLY kind (#2976) tree | commitdiff
2019-04-17 Andrew ReynoldsFix extended function decomposition (#2960) tree | commitdiff
2019-04-16 Andres NoetzliMake bv{add,mul,and,or,xor,xnor} left-associative ... tree | commitdiff
2019-04-16 Andrew ReynoldsMinor simplifications to theory quantifiers (#2953) tree | commitdiff
2019-04-11 Andrew Reynolds Eliminate Boolean ITE within terms, fixes 2947 (#2949) tree | commitdiff
2019-04-04 Haniel BarbosaIgnoring FP benchmarks with "unsafe" sizes unless optio... tree | commitdiff
2019-04-01 Andres NoetzliFP: Fix wrong model due to partial assignment (#2910) tree | commitdiff
2019-03-29 Andrew ReynoldsFix issues in cvc parser (#2901) tree | commitdiff
2019-03-16 Alex OzdemirEnable CryptoMiniSat-backed BV proofs (#2847) tree | commitdiff
2019-03-15 Haniel BarbosaNew beta-reduction for HOL solving (#2869) tree | commitdiff
2019-03-14 Andrew ReynoldsUse zero slope tangent planes for transcendental functi... tree | commitdiff
2019-03-14 Andrew ReynoldsImplement proper semantics for TPTP predicate is_rat... tree | commitdiff
2019-03-12 Andrew Reynolds Move tuple/record update elimination from ppRewrite... tree | commitdiff
2019-01-22 Andrew Reynolds Fix tuple and record CVC printing (#2818) tree | commitdiff
2019-01-22 Andrew Reynolds Fix parsing of overloaded parametric datatype selector... tree | commitdiff
2019-01-17 Andres NoetzliAdd option to print BV constants in binary (#2805) tree | commitdiff
2019-01-16 Andrew ReynoldsFix constant contains ITOS rewrite (#2799) tree | commitdiff
2019-01-15 Andrew Reynolds Fix unsound double abs rewrite rule for FP (#2792) tree | commitdiff
2018-12-14 Andrew Reynolds Fix extended rewriter for binary associative operators... tree | commitdiff
2018-12-11 Andrew ReynoldsRemove alternate versions of mbqi (#2742) tree | commitdiff
2018-12-10 makaimannBoolToBV modes (off, ite, all) (#2530) tree | commitdiff
2018-12-07 Alex OzdemirEnable BV proofs when using an eager bitblaster (#2733) tree | commitdiff
next