ufmg-smite/lean-smt

Issues

• Incorrect translation of duplicate binder names

  #100 opened 5 months ago by dranov
  2

• `Iff` is translated as an uninterpreted function, leading to wrong results

  #121 opened 4 months ago by dranov
  3

• Usage instructions in README give linking errors

  #118 opened 4 months ago by dranov
  3

• Failure to run `lake build smt`

  #115 opened 4 months ago by zhuanhao-wu
  2

• Failing to translate `DecidableEq`

  #97 opened 5 months ago by dranov
  3

• Error when proving two theorems with smt in the same file

  #60 opened 9 months ago by tomaz1502
  1

• Stable

  #74 opened 9 months ago by AdrienChampion
  2

• Move Nat translation into a proof-producing preprocessing tactic

  #27 opened 2 years ago by Vtec234
  1

• Add all QF_BV builtins

  #41 opened 2 years ago by Vtec234
  0

• Issues with transforming QF_BV

  #29 opened 2 years ago by Vtec234
  2

• Define-fun from local declarations

  #23 opened 2 years ago by Vtec234
  0

• Certifying transformations and local definitions

  #34 opened 2 years ago by Vtec234
  0

• Support Vampire

  #25 opened 2 years ago by Vtec234
  0

• Choosing which formulas and terms to encode

  #20 opened 2 years ago by Vtec234
  1