diff --git a/prover/drivers/smt-driver.md b/prover/drivers/smt-driver.md index 280db294a..c3de73f7b 100644 --- a/prover/drivers/smt-driver.md +++ b/prover/drivers/smt-driver.md @@ -141,6 +141,7 @@ module DRIVER-SMT symbol nil { SMTLIB2SortToSort(LOC) } (.Sorts) : SMTLIB2SortToSort(LOC) axiom !N:AxiomName : heap(SMTLIB2SortToSort(LOC), SMTLIB2SortToSort(DATA)) axiom !M:AxiomName : functional(nil { SMTLIB2SortToSort(LOC) }) + axiom !P:AxiomName : constructor(nil { SMTLIB2SortToSort(LOC) }) ) ...