summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-10-20Support rewrite proofs in the theory of arraysrewrite_proofAndres Notzli
2016-08-15Expression sharing on demand in LFSC (replace definitionally equivalent child...ajreynol
2016-08-15Enable bounded set membership with --fmf-bound. Map to term models for bounde...ajreynol
2016-08-12Add a few more regressions.ajreynol
2016-08-12Minor fixes to model construction to take singleton equivalence classes into ...ajreynol
2016-08-12Merge pull request #90 from 4tXJ7f/fewer_preproc_holesguykatzz
2016-08-11Add support for fewer preprocessing holesAndres Notzli
2016-08-11Minor change to strings, introduce proxy vars only when necessary.ajreynol
2016-08-10Improvements to strings: work on propagations for reverse normal form process...ajreynol
2016-08-09Merge pull request #89 from 4tXJ7f/fix_proof_spacesguykatzz
2016-08-09Fixes for sep star rewrite.ajreynol
2016-08-09Fix missing/redundant spaces in proofsfix_proof_spacesAndres Notzli
2016-08-05Merge pull request #88 from 4tXJ7f/fix_commentsguykatzz
2016-08-05Minor: add/fix comments, remove redundant includesAndres Notzli
2016-08-03Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.Guy
2016-08-03Merge pull request #87 from 4tXJ7f/fix_oob_accessbarrettcw
2016-07-30Prioritize inferences when processing normal forms in strings.ajreynol
2016-07-28The "aggressive" optimizer for lemma L now returns the conjunction of all lem...Guy
2016-07-28Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-28Bug fix involving negated lemmasGuy
2016-07-28Fix bug 749.ajreynol
2016-07-28Add the negative conjunction caseGuy
2016-07-27Fix out-of-bounds access in ExprManagerAndres Notzli
2016-07-27Proper instrumentation of the preprocessing phaseGuy
2016-07-27proper handling of ITEsGuy
2016-07-27Proper handling of IFF lemmas in the unsat core.Guy
2016-07-27Added an option for a more aggressive weakest implicant optimizationGuy
2016-07-27If we can't find a weaker implicant, fail gracefully and return the original ...Guy
2016-07-26Merge pull request #86 from 4tXJ7f/fix_warningsguykatzz
2016-07-26Fix warnings in src/proofAndres Notzli
2016-07-26Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-26Bug fix:Guy
2016-07-26Add option to minimize sygus solutions based on using weakest implicants of i...ajreynol
2016-07-26Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-26Letification of BV constantsGuy
2016-07-26Minor improvements to strings related to constant splitting, including a few ...ajreynol
2016-07-26Added functionality to retrieve a lemma's "weakest implicant" in the unsat co...Guy
2016-07-25Bug fixGuy
2016-07-25Propagate the usage of proof let maps into constant disequality proofsGuy
2016-07-25Bug fixGuy
2016-07-25Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-24cleanupGuy
2016-07-24Use letification for the aliasing declarations as well (consequently, print t...Guy
2016-07-24Proper handling for lemmas that are conjuncts:Guy
2016-07-22Minor, error handling for polymorphism + sep logic.ajreynol
2016-07-21Fixes for strings, explanations for constant split propagations, substr under...ajreynol
2016-07-20Infrastructure for storing and printing heap models for separation logic. Ens...ajreynol
2016-07-20Print only instantiations that are in the unsat core when --proof is enabled....ajreynol
2016-07-20Infer conflicts in strings based on abstracting equality as contains. Minor c...ajreynol
2016-07-19Bug fixGuy
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback