Issues

• Support latest LLVM IR version?

  smackers/smack#860 · Filter by author dcavalei opened on Sep 25, 2026

• Unsigned literals of at least 2^63 are emitted as their signed representative, making guards vacuous

  bug
  smackers/smack#856 · Filter by author shaobo-he opened on Aug 27, 2026

• Boogie 3.x reserved identifiers are missing from Naming::BPL_KW

  bug
  smackers/smack#842 · Filter by author shaobo-he opened on Aug 14, 2026

• Add sound models for common C standard-library input and arithmetic functions

  enhancement
  smackers/smack#839 · Filter by author shaobo-he opened on Jul 21, 2026
  1

• Umbrella: make memory-safety checking storage- and property-aware

  bugenhancement
  smackers/smack#838 · Filter by author shaobo-he opened on Jul 20, 2026
  1

• Proposal: LLM-assisted skill for guided SMACK verification

  smackers/smack#837 · Filter by author shaobo-he opened on Jul 19, 2026

• Documentation roadmap

  enhancement
  smackers/smack#828 · Filter by author shaobo-he opened on Jul 6, 2026

• Incorrect modeling of pointer arithmetic/comparison when --integer-encoding=wrapped-integer

  bug
  smackers/smack#804 · Filter by author shaobo-he opened on Feb 24, 2026
  1

• Heads-up: #[start] is being removed

  smackers/smack#802 · Filter by author RalfJung opened on Dec 20, 2024

• llvm2bpl report error when use smack generate boogie code

  smackers/smack#792 · Filter by author Luweicai opened on Dec 23, 2022
  3

• How it can support ensures, requires, invariant API in Rust

  smackers/smack#791 · Filter by author 1vs9 opened on Nov 24, 2022

• Verifying D programs

  smackers/smack#788 · Filter by author roxanaRA opened on Apr 7, 2022

• Leverage instcombine pass

  smackers/smack#780 · Filter by author shaobo-he opened on Mar 1, 2022
  1

• Some Rust Box operation is internally supported by rustc

  smackers/smack#777 · Filter by author shaobo-he opened on Feb 3, 2022
  1

• Verifying Fortran Intrinsic Function ABS

  smackers/smack#775 · Filter by author udwuwenhao opened on Jan 12, 2022

• Multi-language model checking, on inequality modify languages to match correct model?

  smackers/smack#771 · Filter by author SamuelMarks opened on Dec 6, 2021

• Implement a per-allocation-site memory-safety checking

  smackers/smack#768 · Filter by author shaobo-he opened on Nov 17, 2021

• Feature request: Attempt to compute loop bounds. Unroll to bound if possible. Error if not.

  smackers/smack#760 · Filter by author martinlester opened on Oct 7, 2021
  1

• Implement context-sensitive memory model

  enhancement
  smackers/smack#755 · Filter by author shaobo-he opened on Sep 1, 2021
  3

  

• Prune and Parallelize Instrumented Checks

  smackers/smack#751 · Filter by author shaobo-he opened on Aug 12, 2021
  1

• memcpy Merges Regions Unnecessarily

  smackers/smack#749 · Filter by author shaobo-he opened on Aug 12, 2021
  1

• Keep track of whether memory is allocated by Rust's allocator

  enhancement
  smackers/smack#745 · Filter by author keram88 opened on Jul 7, 2021
  

• PhantomData in the Rust model is not needed

  smackers/smack#744 · Filter by author keram88 opened on Jul 2, 2021

• Convert implicit Rust assertions into smack assertions without including the crate

  smackers/smack#739 · Filter by author keram88 opened on Jun 7, 2021

• Incorrect region generation for ptrtoint/inttoptr arguments

  smackers/smack#738 · Filter by author shaobo-he opened on May 19, 2021
  2