summaryrefslogtreecommitdiff
path: root/test/regress/regress0/proofs
AgeCommit message (Expand)Author
2021-10-26[proofs] Fix singleton check in MACRO_RES post-processing (#7498)Haniel Barbosa
2021-10-26[proofs] Reset local var in SatProofManager since incremental exists (#7500)Haniel Barbosa
2021-10-26[proofs] Fix and simplify CHAIN_RESOLUTION checker (#7492)Haniel Barbosa
2021-10-22[proof] Fixing CHAIN_RESOLUTION checker (#7465)Haniel Barbosa
2021-10-21[proofs] Fix open proof in SAT solver due to cycles (#7448)Haniel Barbosa
2021-10-11Connect the LFSC printer (#7323)Andrew Reynolds
2021-07-14bv: Rename simple solver to bitblast-internal. (#6888)Mathias Preiner
2021-07-14[proof] Fix open proof issues in SAT proof (#6887)Haniel Barbosa
2021-07-14Add option that exercises the previously buggy behavior (#6884)Haniel Barbosa
2021-07-14Fix for context on input proof generator (#6873)Andrew Reynolds
2021-07-13[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)Haniel Barbosa
2021-06-07(proof-new) Fix missing connection in trust substitution proofs (#6685)Andrew Reynolds
2021-06-02Fix issues with double negation in circuit propagator (#6669)Gereon Kremer
2021-04-07[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback