From 65686d99c47e84712ed6d276c8deb75901f6487d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 5 Apr 2024 11:59:54 -0500 Subject: [PATCH] More --- user_manual.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/user_manual.md b/user_manual.md index 9e97687f..4a1e5330 100644 --- a/user_manual.md +++ b/user_manual.md @@ -875,11 +875,11 @@ An example use case for this feature is directly refer to the nil terminator of > If no free parameters are used in the nil terminator of a parameterized constant, then it is treated equivalent to if it were declared via an ordinary declare-const command. -For example: +The following are examples of list operations when using parameterized constant `bvor`: ``` (declare-const a (BitVec 4)) (declare-const b (BitVec 4)) -(declare-const c (BitVec 4)) +(declare-const c (BitVec 5)) (alf.nil bvor) == (alf.nil bvor) ; since we cannot infer the type of bvor (alf.nil bvor a) == #b0000 ; since #b0000 is the nil terminator of (bvor a)