summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-20Fix Arith lemmas for div/modfixArithLemmasPRAndres Noetzli
2020-05-20Normal form equality conflicts and uniqueness check (#4497)Andrew Reynolds
2020-05-20Add proof skolem cache (#4485)Andrew Reynolds
2020-05-20Fix parametric datatype instantiation (#4493)Andrew Reynolds
2020-05-20CegqiBv: Clean up after renaming options. (#4487)Aina Niemetz
2020-05-20Use debug-check-model to enable internal debugging in check-model (#4480)Andrew Reynolds
2020-05-19Add a simple script to convert sygus v1 files to v2. (#4409)Abdalrhman Mohamed
2020-05-19Do not eliminate variables that are equal to unevaluatable terms (#4267)Andrew Reynolds
2020-05-19Fix cached free variable identifiers in sygus term database (#4394)Andrew Reynolds
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-05-19Use fresh variables when miniscoping (#4296)Andrew Reynolds
2020-05-19Update enum and option names for sygus languages (#4388)Andrew Reynolds
2020-05-19Make SolveEq and PlusCombineLikeTerms idempotent (#4438)Andres Noetzli
2020-05-12Do not enable unconstrained simplification if arithmetic is present (#4489)Andrew Reynolds
2020-05-06Update run scripts for SMT-COMP 2020 (#4454)Andres Noetzli
2020-05-05Always introduce fresh variable for unconstrained APPLY_UF (#4472)Andrew Reynolds
2020-05-05Update copyright year and AUTHORS/THANKS files. (#4468)Aina Niemetz
2020-05-01SMT-COMP 2020: Enable --fp-exp for new FP logics. (#4432)Aina Niemetz
2020-05-01Move slow regression to regress3 (#4430)Andrew Reynolds
2020-04-30Fix regression (#4424)Andrew Reynolds
2020-04-30Remove skolem share involving pre_first_ctn. (#4423)Andrew Reynolds
2020-04-30Do not mark congruent terms are reduced (#4419)Andrew Reynolds
2020-04-29SMT-COMP 2020: Fix scripts to use --no-type-checking instead of --no-checking...Aina Niemetz
2020-04-29Avoid circular dependencies for justifying reductions in strings extf eval (#...Andrew Reynolds
2020-04-29Fix strings 2.6 regression (#4413)Andrew Reynolds
2020-04-28Register lower bound for str.to_int (#4408)Andres Noetzli
2020-04-28Updates to SMT COMP script for 20 minute timeout (#4406)Andrew Reynolds
2020-04-28update Haniel's affiliation (#4404)Haniel Barbosa
2020-04-28contrib/get-gmp: Rename and update install instructions with a warning. (#4407)Aina Niemetz
2020-04-28Support the SMT-LIB Unicode string standard by default (#4378)Andrew Reynolds
2020-04-28Update cardinality in strings to unicode standard (#4402)Andrew Reynolds
2020-04-27Fix sygus unit (#4371)Andrew Reynolds
2020-04-27Fix examples instructions in INSTALL.md. (#4397)Mathias Preiner
2020-04-25 Fix sets cardinality cycle rule (#4392)Andrew Reynolds
2020-04-23Introduce best content heuristic for strings (#4382)Andres Noetzli
2020-04-22Strings: Register skolems before sending lemma (#4381)Andres Noetzli
2020-04-22Ensure disequality splits are processed as lemmas (#4380)Andrew Reynolds
2020-04-22Allow eager bitblasting with solve bv as int in QF_NIA (#4373)Andrew Reynolds
2020-04-22Convert V2.5 SMT regressions to V2.6. (#4319)Abdalrhman Mohamed
2020-04-22Reinstantiate support for conjunctions in facts (#4377)Andres Noetzli
2020-04-21Update to sygus version 2 (#4372)Andrew Reynolds
2020-04-21Fix for parse options related to binary name (#4368)Andrew Reynolds
2020-04-20Introduce a public interface for Sygus commands. (#4204)Abdalrhman Mohamed
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-20Refactor inference manager in strings to be amenable to proofs (#4363)Andrew Reynolds
2020-04-20Add SCOPE proof rule (#4332)Andrew Reynolds
2020-04-18Disable unsat cores on nec regression (#4330)Andrew Reynolds
2020-04-18Track inference id for pending facts in strings (#4331)Andrew Reynolds
2020-04-18Improving EqProof printing (#4329)Haniel Barbosa
2020-04-17Add (context-dependent) Proof (#4323)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback