boogie-org/corral

Issues

• Which tests should we run in CI?

  #164 opened 2 years ago by rakamaric
  1

• Release for NET6

  #161 opened 2 years ago by m-carrasco
  0

• Cannot set nuget key for automatic deployment

  #156 opened 3 years ago by zvonimir
  7

• BinaryFormatter is obsolete in .NET 5.0 (warning issued)

  #154 opened 3 years ago by zvonimir
  0

• Duality / FixedPointVC regressions

  #136 opened 3 years ago by akashlal
  12

• bogus PRs

  #148 opened 3 years ago by akashlal
  8

• Unintended consequences of wrapping assertions into one single function

  #138 opened 3 years ago by zvonimir
  3

• "Turning off Z3 search due to parallel assignments" message meaning?

  #135 opened 4 years ago by hayley-leblanc
  2

• Updating AV regressions

  #133 opened 4 years ago by akashlal
  2

• Using Boogie nuget

  #130 opened 4 years ago by akashlal
  3

• AV: fastavn: print stats when times out?

  #59 opened 4 years ago by shaobo-he
  3

• AV: Blowup for multi arity maps

  #61 opened 6 years ago by shuvendu-lahiri
  1

• AV: flag `/entryPointExcludes` is broken

  #57 opened 7 years ago by shaobo-he
  1

• Gitversion warning

  #115 opened 4 years ago by akashlal
  2

• Abstract Houdini removed from Boogie

  #127 opened 4 years ago by zvonimir
  5

• Internal bug: Refinement unable to make progress

  #125 opened 4 years ago by unboxedtype
  2

• Corral crashes on a program

  #124 opened 4 years ago by shaobo-he
  0

• Switching Corral to use lit for running regressions

  #121 opened 4 years ago by zvonimir
  2

• Corral crashing when thread id is bv32

  #109 opened 4 years ago by zvonimir
  3

• Nonlinear arithmetic incompleteness?

  #100 opened 4 years ago by prgantonino
  4

• use of assume forall in corral

  #112 opened 4 years ago by muyaview
  3

• question on exists clause

  #97 opened 4 years ago by muyaview
  2

• Z3 fixedpoint module and its usage in Boogie/Corral

  #88 opened 4 years ago by zvonimir
  5

• Corral doesn't support polymorphic type constructor

  #117 opened 4 years ago by Invincibleyc
  3

• Corral reports "no bugs" when there is no prover found

  #114 opened 4 years ago by zvonimir
  0

• Switching from Z3 4.8.5 to 4.8.6 leads to major issues

  #110 opened 5 years ago by zvonimir
  2

• Crash with "Must find a successor" exception

  #55 opened 7 years ago by zvonimir
  7

• Use of axioms in corral

  #99 opened 5 years ago by prgantonino
  2

• Handling stubs with modifies

  #98 opened 5 years ago by shuvendu-lahiri
  2

• Understanding the output of /printAllTraces?

  #82 opened 5 years ago by bitcalc
  1

• Cannot build Corral commit 88b7f62

  #85 opened 5 years ago by shaobo-he
  1

• invariant statements is not supported?

  #96 opened 5 years ago by muyaview
  19

• Command line option descriptions?

  #83 opened 5 years ago by bitcalc
  1

• Printing variable values

  #95 opened 5 years ago by prgantonino
  2

• multi-threads of Corral?

  #81 opened 5 years ago by bitcalc
  2

• running tests on MacOS

  #92 opened 5 years ago by shazqadeer
  1

• Unable to run corral.exe on Mac

  #93 opened 5 years ago by shazqadeer
  2

• Cannot build Corral

  #89 opened 5 years ago by garbervetsky
  1

• Loop bound estimation and loop abstraction?

  #80 opened 6 years ago by bitcalc
  6

• Using /di flag it seems causes an assertion violation to be missed

  #79 opened 6 years ago by zvonimir
  0

• Corral produces trace for sdvdefectviewer directly

  #78 opened 6 years ago by shuvendu-lahiri
  2

• Corral variable abstraction refinement yields ill-formed intermediate program for multi-dimensional arrays

  #77 opened 6 years ago by shuvendu-lahiri
  0

• AV: PropInst matching against non-source lines

  #76 opened 6 years ago by shuvendu-lahiri
  0

• AV property files cannot refer to undeclared functions and variables

  #75 opened 6 years ago by shuvendu-lahiri
  2

• AV: Null dereference

  #71 opened 6 years ago by rcastano
  1

• Incorrect order when using {:ProgramInitialization} attribute

  #73 opened 6 years ago by garbervetsky
  2

• AV: Problem with generalization of repetead fields

  #70 opened 6 years ago by rcastano
  1

• Map assignments don't seem to be supported by AliasAnalysis

  #69 opened 6 years ago by rcastano
  1

• AV: PropInst fails to instrument Ref types for TinyBCT files

  #67 opened 6 years ago by shuvendu-lahiri
  0

• Corral fails to take into account /bopt:proverOpt:OPTIMIZE_FOR_BV=true

  #63 opened 6 years ago by zvonimir
  7