From: Aina Niemetz Date: Tue, 15 Jun 2021 18:46:22 +0000 (-0700) Subject: docs: Fix reference in sep logic reference. (#6747) X-Git-Tag: cvc5-1.0.0~1601 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09e438c6e6d10e0ad1e7c3e3de39ed4eb1d48ee1;p=cvc5.git docs: Fix reference in sep logic reference. (#6747) --- diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst index 43c114404..86f802ef8 100644 --- a/docs/theories/separation-logic.rst +++ b/docs/theories/separation-logic.rst @@ -8,7 +8,7 @@ Signature --------- Given a (decidable) base theory :math:`T`, cvc5 implements a decision procedure -for quantifier-free :math:`SL(T)_{Loc,Data}` formulas :cite:`ReynoldsIS016`, +for quantifier-free :math:`SL(T)_{Loc,Data}` formulas :cite:`ReynoldsISK16`, where :math:`Loc` and :math:`Data` are any sort belonging to :math:`T`. A :math:`SL(T)_{Loc,Data}` formula is one from the following grammar: