boogie-org/boogie

Issues

• [Civl] Paxos proof depends on unchecked assumption

  #949 opened 2 months ago by shazqadeer
  1

• Standalone binary

  #944 opened 3 months ago by wrwg
  11

• Are VcOutcome.ReachedBound and CommandLineOptions.RecursionBound obsolete?

  #936 opened 3 months ago by shazqadeer
  1

• Bitwise operations make the SMT solver run infinitely

  #940 opened 3 months ago by radumcostache
  4

• Irreducible control flow graphs

  #921 opened 4 months ago by petemud
  9

• {:inline 0} is inconsistent

  #933 opened 4 months ago by petemud
  4

• Tests time out non-deterministically

  #909 opened 4 months ago by keyboardDrummer
  6

• [Civl] Better method for hoisting asserts in an atomic action

  #903 opened 4 months ago by shazqadeer
  1

• Let pruning also prune 'TypeCtorDecl' declarations

  #916 opened 4 months ago by keyboardDrummer
  0

• Enable modular resolution/preprocessing of Boogie programs

  #889 opened 6 months ago by keyboardDrummer
  0

• Replace call-stack based AST traversal code with heap-stack based traversal

  #711 opened 2 years ago by keyboardDrummer
  3

• ProverException: Prover died with no further output, perhaps it ran out of memory or was killed.

  #879 opened 7 months ago by NamrathaG
  1

• Civl: Hints not being carried over into the cooperation checker

  #867 opened 7 months ago by hrishikesh-bk
  0

• Possibly Missing Interpolation in SMTLibInteractiveTheoremProver

  #863 opened 8 months ago by Marti2203
  2

• Low values of :rlimit have no effect

  #801 opened a year ago by robin-aws
  0

• Verification fails in the presence of a dummy/unused function

  #824 opened a year ago by zhassan-aws
  4

• /prune removes relevant information

  #819 opened a year ago by glor
  0

• SMT errors when running without `/prune`

  #813 opened a year ago by atomb
  0

• Some SMT from monomorphic encoding rejected by CVC5

  #799 opened a year ago by atomb
  0

• Boogie doesn't send `timeLimit` to CVC5

  #798 opened a year ago by atomb
  0

• CVC5 works only with batch mode

  #797 opened a year ago by atomb
  2

• Boogie fails to parse certain `unknown` responses

  #803 opened a year ago by atomb
  0

• :rlimit value multiplied by 1000 when passed to prover

  #795 opened a year ago by robin-aws
  2

• Prover error: ; :rlimit line: 64 position: 1

  #784 opened a year ago by 0sidharth
  2

• Boogie not Terminating with Prune on

  #791 opened a year ago by yizhou7
  7

• Is there any up-to-date language reference?

  #779 opened a year ago by glor
  2

• Inconsistent printing of type synonyms that use builtins

  #775 opened a year ago by zafer-esen
  2

• Abstract interpretation ignores where clauses

  #786 opened a year ago by RustanLeino
  0

• Don't support << or >> shift operations in move language.

  #785 opened a year ago by oday0311
  2

• `NullReferenceException` in `VC.Split.PrintTopLevelDeclarationsForPruning`

  #639 opened a year ago by cpitclaudel
  3

• Exception when Boogie exits

  #733 opened 2 years ago by shazqadeer
  6

• Persistent caching of verification results

  #762 opened a year ago by emugnier
  4

• Option /causalImplies does not exist

  #757 opened a year ago by totoyoyo
  1

• Missing constructor type arguments in auto-generated map axioms

  #756 opened a year ago by atomb
  0

• Inconsistency in predicate-based map axioms when using MBQI

  #735 opened a year ago by atomb
  20

• Refactor call desugaring and passive command creation

  #743 opened a year ago by atomb
  5

• Pruning removes too much

  #747 opened a year ago by atomb
  5

• Allow any construct to be tracked by "necessary assumptions"

  #730 opened a year ago by atomb
  2

• CVC5 support?

  #737 opened a year ago by hmijail
  3

• Crash when Boogie receives SIGINT

  #716 opened 2 years ago by keyboardDrummer
  0

• Check consistency of function parameter names in API

  #702 opened 2 years ago by RustanLeino
  0

• Set exit code to non-zero when verification fails

  #695 opened 2 years ago by atomb
  3

• Deadlock in CheckerPool when maxKeepGoingSplits is used

  #675 opened 2 years ago by rakamaric
  2

• Boogie generates cvc5 incompatible smt2 syntax without monomorphize

  #659 opened 2 years ago by ChuyueSun
  16

• Fix trace timings when `vcsCores > 1`

  #674 opened 2 years ago by cpitclaudel
  0

• Emit axioms only for theories used by queries

  #660 opened 2 years ago by atomb
  0

• boogie generated synatically wrong smt2

  #643 opened 2 years ago by ChuyueSun
  1

• Unexplainable absence of Model and `{:print}` instructions

  #620 opened 2 years ago by wrwg
  17

• /monomorphize crashes "internal error, shallow-type assignment was done incorrectly"

  #613 opened 2 years ago by gauravpartha
  2

• Incomplete map expressions in the Boogie output

  #609 opened 2 years ago by junkil-park
  5