[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