From f4b143bdde05d8ff97d852a3535765f914fbe663 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Mon, 4 May 2020 16:40:44 -0500 Subject: [PATCH] smt-driver: nil is a constructor --- prover/drivers/smt-driver.md | 1 + 1 file changed, 1 insertion(+) 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) }) ) ...