Description

CatarinaGamboa

opened on Oct 8, 2026

Issue body actions

In the following example, having the path conditions there and then true makes it seem like the value of the variable is true and not the refinement is true, and it's not really useful information for a developer.

Activity

1. CatarinaGamboa

   added

   enhancementNew feature or requestNew feature or request

   on Oct 8, 2026
2. CatarinaGamboa commented on Nov 2, 2026

   

   CatarinaGamboa

   on Nov 2, 2026

   CollaboratorAuthor

   More actions

   Another example from the error-message study, the JabRef EditAction exercise: undoManager.redo() inside a switch case, where undoManager comes from a getter. Found shows five path-condition binders before the one row that matters, and four of them are only true:

   ∀getUndoManager⁸⁵⁶   true →
   ∀#fresh⁸³⁸           true →
   ∀#fresh⁸³⁹           !#fresh⁸³⁸ →
   ∀#fresh⁸⁵¹           true →
   ∀#fresh⁸⁵²           true →
   ∀#fresh⁸⁵³           !(#fresh⁸⁵¹ || #fresh⁸⁵²) →
   ∀undoManager⁸⁵⁸      undoManager⁸⁵⁸ == getUndoManager⁸⁵⁶
   

   None of these say anything about the expected redoable(undoManager⁸⁵⁸). Field binders with only true have the same problem (#457).

   In VS Code:

   
3. CatarinaGamboa

   added

   studyNeeded before the error-message user studyNeeded before the error-message user study

   on Nov 2, 2026
4. CatarinaGamboa

   added 2 commits that reference this issue on Nov 3, 2026

   Drop true binders the error does not need and write fields as in code (…

   70edf72

   Drop true rows for variables that another row of Found already shows (#…

   926f027
5. CatarinaGamboa

   closed this as completedin #476on Nov 4, 2026
6. CatarinaGamboa

   added a commit that references this issue on Nov 5, 2026

   Drop path conditions that expected does not depend on from Found (#487)

   93c331c

Issue actions