Search results

Cannot translate <code>nat_lit</code> due to <code>Nat.add</code>

Status: Open.

#185 In ufmg-smite/lean-smt;

· dranov opened on Jun 19, 2025

Issues with cvc5 ffi when building

Status: Open.

#173 In ufmg-smite/lean-smt;

· FrederickPu opened on Apr 18, 2025

<code>abbrev</code> types are translated incorrectly

Status: Open.

#141 In ufmg-smite/lean-smt;

· dranov opened on Nov 6, 2024

<code>Iff</code> is translated as an uninterpreted function, leading to wrong results

Status: Open.

#121 In ufmg-smite/lean-smt;

· dranov opened on Jul 8, 2024

Incorrect translation of duplicate binder names

Status: Open.

#100 In ufmg-smite/lean-smt;

· dranov opened on May 23, 2024

Certifying transformations and local definitions

Status: Open.

#34 In ufmg-smite/lean-smt;

· Vtec234 opened on Jul 6, 2022

Move Nat translation into a proof-producing preprocessing tactic

Status: Open.

#27 In ufmg-smite/lean-smt;

· Vtec234 opened on Jun 24, 2022

Choosing which formulas and terms to encode

Status: Open.

#20 In ufmg-smite/lean-smt;

· Vtec234 opened on Jun 15, 2022