Index

B

block preserved

C

config file

CVL

F

file config

first-order logic formal-verification

G

gambit ghost initial state variable

H

helper variables

hook

L

logic first-order operators propositional

loop optimistic

O

operators logical

optimistic_loop over-approximation

P

parametric rules preconditions predicate logic

predicates preserved block propositional logic propositions

Q

quantifiers

R

revert rule vacuous

rules parametric

V

vacuity, [1] vacuous

variables cvl

W

withrevert