Issues

• Soundness: the arguments type encoding's reverse casts are unguarded

  boogie-org/boogie#1168 · Filter by author erniecohen opened on Sep 26, 2026

• [Civl] Introducing preconditions/assume statements breaks refinement

  boogie-org/boogie#1153 · Filter by author maul-esel opened on Aug 24, 2026
  5

• NullReferenceException at resolve time: a call inside a code expression in a procedure specification

  boogie-org/boogie#1148 · Filter by author shaobo-he opened on Aug 13, 2026

• Soundness: CIVL layer rewriting can smuggle an illegal global loop invariant past type checking

  boogie-org/boogie#1146 · Filter by author shaobo-he opened on Aug 10, 2026

• Soundness: focus + split_here can turn a failing pre-split assertion into an assumption

  boogie-org/boogie#1145 · Filter by author shaobo-he opened on Aug 10, 2026
  1

• :msg with trace

  boogie-org/boogie#1132 · Filter by author mira-alford opened on May 26, 2026
  2

• Duplicate SMT assert names with /warnVacuousProofs

  boogie-org/boogie#1116 · Filter by author agle opened on Apr 10, 2026
  

• Small BoogiePL grammar ambiguities

  boogie-org/boogie#1114 · Filter by author katrinafyi opened on Mar 21, 2026

• [Civl] Layer inference

  boogie-org/boogie#1101 · Filter by author shazqadeer opened on Feb 9, 2026

• [Civl] Fix type checking of parallel calls

  boogie-org/boogie#1077 · Filter by author shazqadeer opened on Nov 15, 2025
  1

• [Civl] Generalized yield invariants

  boogie-org/boogie#1067 · Filter by author shazqadeer opened on Oct 29, 2025

• Trivial copy assignment (y := x) is omitted from SMT named assumes → missing from unsat cores / coverage

  boogie-org/boogie#1066 · Filter by author ricostynha1 opened on Oct 27, 2025
  1

  

• Updated Documentation?

  boogie-org/boogie#1000 · Filter by author TateStaples opened on Feb 17, 2025
  4

• Bitwise operations make the SMT solver run infinitely

  boogie-org/boogie#940 · Filter by author radumcostache opened on Aug 15, 2024
  4

• Let pruning also prune 'TypeCtorDecl' declarations

  enhancement
  boogie-org/boogie#916 · Filter by author keyboardDrummer opened on Jul 22, 2024

• Tests time out non-deterministically

  boogie-org/boogie#909 · Filter by author keyboardDrummer opened on Jul 17, 2024
  6

• Enable modular resolution/preprocessing of Boogie programs

  enhancement
  boogie-org/boogie#889 · Filter by author keyboardDrummer opened on May 23, 2024

• /prune removes relevant information

  boogie-org/boogie#819 · Filter by author glor opened on Nov 29, 2023

• SMT errors when running without /prune

  bug
  boogie-org/boogie#813 · Filter by author atomb opened on Nov 21, 2023

• Low values of :rlimit have no effect

  boogie-org/boogie#801 · Filter by author robin-aws opened on Oct 18, 2023
  

• Some SMT from monomorphic encoding rejected by CVC5

  bug
  boogie-org/boogie#799 · Filter by author atomb opened on Oct 16, 2023
  

• Boogie doesn't send timeLimit to CVC5

  bug
  boogie-org/boogie#798 · Filter by author atomb opened on Oct 16, 2023
  

• CVC5 works only with batch mode

  bug
  boogie-org/boogie#797 · Filter by author atomb opened on Oct 16, 2023
  2

  

• Abstract interpretation ignores where clauses

  boogie-org/boogie#786 · Filter by author RustanLeino opened on Sep 22, 2023

• Persistent caching of verification results

  boogie-org/boogie#762 · Filter by author emugnier opened on Jul 11, 2023
  4