Bug in the translation of `Std.BitVec.not`

[shigoel]

Here is an example to illustrate the issue:

import Std.Data.BitVec
import Auto

set_option auto.smt true
set_option auto.smt.trust true
set_option trace.auto.smt.printCommands true
set_option trace.auto.smt.result true

open Std.BitVec

theorem bvnot_auto_test (x : Std.BitVec 4) :
  x + (Std.BitVec.not x) = 0xF#4 := by
  auto

The error message is:

[auto.smt.result] SMT invocation failed with lamTerm2STerm :: The arity of Auto.Embedding.Lam.LamBaseTerm.bvcst (.bvnot 4) is not 1

[PratherConid]

@shigoel Thanks for finding the bug! I've pushed a fix. Let me know if it's not working or any new issues pop up.

[PratherConid]

But for more involved issues I might not be able to respond before Jan 7th next year.