Skip to content
This repository has been archived by the owner on Apr 27, 2024. It is now read-only.

Repository containing the SMT queries generated during the verification of the `LongMap`.

Notifications You must be signed in to change notification settings

epfl-lara/LongMap-SMT-queries

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

3 Commits
 
 
 
 
 
 

Repository files navigation

LongMap-SMT-queries

This repository contains the SMT queries generated during the verification of the LongMap TODO ADD LINK TO BOLTS.

The file VCs_summary_nocache.csv contains the list of the VCs with the following columns:

  • SMT Query ID: The ID of the corresponding SMT-lib file in the smt-queries-longmap folder.
  • Position: The position of the corresponding line in the source code.
  • Function: The name of the function the VC corresponds to.
  • VC Details: The details of what the VC verifies.
  • Validity: The validity of the VC, either valid, or trivial. trivial means the VC is trivially valid after being simplified by Stainless' simplifier, without being sent to an SMT solver.
  • Solver: The SMT solver that verified the VC the quickest among z3, cvc4, and cvc5.
  • Solving Time (sec): The time required to solve the VC by the solver in seconds.

About

Repository containing the SMT queries generated during the verification of the `LongMap`.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages