Search results

Invalid Triggers via Subslicing

bugSomething isn't workingSomething isn't working

encoding

invalidThis doesn't seem rightThis doesn't seem right

triggers

Status: Open.

#1030 In viperproject/gobra;

· ArquintL opened on May 13, 2026

Precondition of Outline Stmt Rejected

bugSomething isn't workingSomething isn't working

type checking

Status: Open.

#1029 In viperproject/gobra;

· ArquintL opened on May 13, 2026

Gobra does not immediately realize semantics of copying arrays by assignment

bugSomething isn't workingSomething isn't working

encoding

incompleteness

Status: Open.

#1027 In viperproject/gobra;

· felixlinker opened on May 6, 2026

Can prove nil-ness and non-nilness from struct predicate

documentationImprovements or additions to documentationImprovements or additions to documentation

Status: Open.

#1025 In viperproject/gobra;

· felixlinker opened on May 4, 2026

Incomplete Slice Allocation Spec

encoding

enhancementNew feature or requestNew feature or request

Status: Open.

#1007 In viperproject/gobra;

· ArquintL opened on Mar 4, 2026

Parser Error for Reserved Keywords

enhancementNew feature or requestNew feature or request

parsing

Status: Open.

#1005 In viperproject/gobra;

· ArquintL opened on Mar 2, 2026

Allow impure assertions for assert by

enhancementNew feature or requestNew feature or request

Status: Open.

#999 In viperproject/gobra;

· ArquintL opened on Feb 24, 2026

Invalid SMT Encoding

bugSomething isn't workingSomething isn't working

encoding

Status: Open.

#997 In viperproject/gobra;

· ArquintL opened on Feb 20, 2026

Unintuitive semantics for mixed non-hyper-predicates and hyper-predicates

documentationImprovements or additions to documentationImprovements or additions to documentation

SIF

Status: Open.

#996 In viperproject/gobra;

· felixlinker opened on Feb 17, 2026

Using rel(t,0) < rel(t,1) with implication in SIF mode causes an error.

Status: Open.

#994 In viperproject/gobra;

· AkasakaJelos opened on Feb 11, 2026

Assert might fail even defined before the ghost if block in hypermode using rel()

Status: Open.

#993 In viperproject/gobra;

· AkasakaJelos opened on Feb 6, 2026

Cross execution access bug in rel() and ghost if blocks

Status: Open.

#992 In viperproject/gobra;

· AkasakaJelos opened on Feb 4, 2026