[SMT-LIB] What does "c::main::1::IN!0 at 1#0" mean in a SMT-lib file?
Martin Brain
martin.brain at cs.ox.ac.uk
Thu Dec 17 11:50:06 EST 2015
On Thu, 2015-12-17 at 08:37 -0800, Zhoulai wrote:
> Hello, I come across this statement in a SMT-lib file:
> (define-fun t () (_ FloatingPoint 8 24) |c::main::1::IN!0 at 1#0|)
>
> Can anyone explains to me on the '|c::main::1::IN!0 at 1#0|' part? Thanks.
It is the name of another variable; it looks like the names generated by
CBMC. | is used as a quote character.
Cheers,
- Martin
More information about the SMT-LIB
mailing list