Search results

Forward goto after variable declaration causes crash

Status: Open.

#991 In viperproject/silicon;

· fosslinux opened on Jul 10, 2026

Doing bitvector work in cvc5 puts the solver in a broken state

Status: Open.

#990 In viperproject/silicon;

· fosslinux opened on Jul 10, 2026

Conjunction of abstract functions is not able to be asserted

Status: Open.

#989 In viperproject/silicon;

· fosslinux opened on Jul 10, 2026

Wands are not checked for self-framingness

magic-wands

Status: Open.

#974 In viperproject/silicon;

· marcoeilers opened on May 7, 2026

Asserting after assuming quantifier with heap-dependent trigger fails

bugSomething isn't workingSomething isn't working

incompleteness

quantified-permissions

Status: Open.

#959 In viperproject/silicon;

· mschwerhoff opened on Jan 15, 2026

A potential bug in how Silicon handles loop invariant

Status: Open.

#957 In viperproject/silicon;

· funemy opened on Dec 9, 2025

Internal function preconditions not assumed in wand-related scenario

incompleteness

Status: Open.

#951 In viperproject/silicon;

· marcoeilers opened on Nov 24, 2025

Something is wrong with predicate triggers for functions

unsoundness

Status: Open.

#925 In viperproject/silicon;

· marcoeilers opened on May 20, 2025

Information following from field access receiver not known when checking for permission

incompleteness

Status: Open.

#912 In viperproject/silicon;

· marcoeilers opened on Mar 20, 2025

NumberFormatException when Enabling Counterexamples

Status: Open.

#902 In viperproject/silicon;

· ArquintL opened on Mar 3, 2025

Method only verifies with --useOldAxiomatization

Status: Open.

#855 In viperproject/silicon;

· superaxander opened on Jun 19, 2024

Lots of tests fail with --conditionalizePermissions

Status: Open.

#851 In viperproject/silicon;

· marcoeilers opened on Jun 13, 2024