viperproject/silicon

Issues

• State merging failed: unexpected mismatch between symbolic states

  #862 opened 2 months ago by zgrannan
  1

• Unfolding seems to be missing when asserting function

  #873 opened 3 months ago by bobismijnnaam
  3

• Confusing behaviour with `perm` in a quantifier for quantified vs non-quantified fields

  #868 opened 4 months ago by superaxander
  2

• Questions about maintaining solver's context when adding parallelism in silicon

  #861 opened 4 months ago by fanweneddie
  3

• Incompleteness for heap-dependent functions with quantified permissions

  #856 opened 6 months ago by jwkai
  3

• Function applications with `unfolding` not inferred to be equal

  #858 opened 6 months ago by bobismijnnaam
  2

• Trigger warning might cause slow and failing verification

  #857 opened 6 months ago by mschwerhoff
  0

• `FuncApp` in axioms

  #847 opened 7 months ago by pieter-bos
  3

• Method only verifies with --useOldAxiomatization

  #855 opened 6 months ago by superaxander
  0

• Lots of tests fail with --conditionalizePermissions

  #851 opened 7 months ago by marcoeilers
  0

• Weird behavior if WorkerBorrowingForkJoinWorkerThread.onStart throws an InterruptedException

  #850 opened 7 months ago by marcoeilers
  0

• Unrelated fold removes knowledge of quantifier with predicate unside

  #844 opened 7 months ago by sakehl
  2

• Does not regonize heap dependent function as trigger

  #845 opened 7 months ago by sakehl
  2

• Unsoundness related to QPs with unsatisfiable conditions

  #842 opened 8 months ago by marcoeilers
  2

• Unsound behavior with QPs without condition

  #833 opened 8 months ago by marcoeilers
  0

• Incorrect error message for method call on field access

  #830 opened 8 months ago by rayman2000
  3

• Apparent wildcard and possibly QP related incompleteness

  #816 opened 8 months ago by marcoeilers
  1

• Quantifier with predicates/predicates with quantifiers interfere with each other

  #832 opened 8 months ago by sakehl
  4

• Multiple quantifiers to memory locations of same type

  #831 opened 8 months ago by sakehl
  4

• Obviously true precondition "doesn't hold" when using predicate

  #826 opened 9 months ago by ArmborstL
  1

• Using --help crashes Silicon (again)

  #819 opened 9 months ago by marcoeilers
  0

• Reporting multiple errors

  #735 opened 10 months ago by fpoli
  5

• Potential unsoundness

  #810 opened 10 months ago by marcoeilers
  0

• Function body needs to be asserted manually

  #803 opened a year ago by dnezam
  2

• Tests non-deterministically time out

  #801 opened a year ago by Dspil
  0

• Incompleteness when exhaling a QP whose permission expression depends on the quantified variable inside a package statement

  #796 opened a year ago by marcoeilers
  0

• Unsound axiom not considered when domain not used

  #793 opened a year ago by bruggerl
  1

• Slow verification with: well-formedness checks within a big disjunction

  #791 opened a year ago by bobismijnnaam
  3

• Slow verification with trivial quantified permissions

  #788 opened a year ago by bobismijnnaam
  2

• Strange output when reporting quantifier instantiations using newer Z3 versions

  #786 opened a year ago by dnezam
  1

• Unexpected assertion failure when using --setAxiomatizationFile without axioms and variables

  #779 opened a year ago by dnezam
  0

• Unexpected assertion failure when using --setAxiomatizationFile without axioms

  #777 opened a year ago by dnezam
  0

• Decreases leads to error with nested quantified permission

  #768 opened a year ago by sakehl
  1

• Errors caused by refute statement inside of loop with goto

  #773 opened a year ago by bruggerl
  2

• Map-related unsoundness

  #769 opened a year ago by marcoeilers
  0

• Uninterpreted functions: postconditions vs axioms

  #765 opened a year ago by fpoli
  2

• --numberOfParallelVerifiers 0 causes NPE

  #726 opened a year ago by alexanderjsummers
  1

• Missing hashCode definitions

  #723 opened a year ago by fpoli
  2

• Domain axioms not instantiated for all relevant cases

  #753 opened a year ago by marcoeilers
  3

• Using domains with interpretations for Perm together with --prover=Z3-API crashes

  #751 opened a year ago by sakehl
  1

• Unrolling loops blows up verification time

  #747 opened a year ago by sakehl
  6

• Crash with "unknown function/constant"

  #749 opened a year ago by marcoeilers
  1

• Recommended stack size

  #748 opened a year ago by pieter-bos
  1

• Definitions of function applications in postconditions of recursively called functions available too late

  #744 opened a year ago by marcoeilers
  1

• Unsoundness due to loop invariant

  #740 opened a year ago by bruggerl
  2

• Viper command line not giving termination error

  #742 opened a year ago by BenjaminFrei
  2

• Unsoundness when using let-expressions inside quantifiers.

  #736 opened a year ago by marcoeilers
  0

• Efficient solver initialization by cloning

  #731 opened 2 years ago by fpoli
  10

• When is the Position of an AST node mandatory?

  #732 opened 2 years ago by fpoli
  6

• Without --enableTempDirectory, --proverLogFile is ignored

  #717 opened 2 years ago by alexanderjsummers
  0