vc_eqExpr two booleans

24 views

Skip to first unread message

Jingyue Wu

unread,

Dec 8, 2012, 5:16:23 PM12/8/12

to stp-...@googlegroups.com

STP's C interface doesn't seem able to create an "EQ" expression on two booleans. Is this expected?

I enclosed a test case, which throws a segfault in BitVector_equal:

Program received signal SIGSEGV, Segmentation fault.

0x000000000041ba30 in BitVector_equal ()

(gdb) bt

#0 0x000000000041ba30 in BitVector_equal ()

#1 0x0000000000505ab0 in BEEV::NonMemberBVConstEvaluator(BEEV::STPMgr*, BEEV::Kind, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&, unsigned int) ()

#2 0x0000000000506745 in BEEV::NonMemberBVConstEvaluator(BEEV::ASTNode const&) ()

#3 0x0000000000468c1d in SimplifyingNodeFactory::CreateNode(BEEV::Kind, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&) ()

#4 0x00000000004368c2 in NodeFactory::CreateNode(BEEV::Kind, BEEV::ASTNode const&, BEEV::ASTNode const&, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&) ()

#5 0x0000000000407dfb in vc_eqExpr ()

#6 0x00000000004067fd in main (argc=<optimized out>, argv=<optimized out>)

at test2.cpp:14

Jingyue

test2.cpp

Vijay Ganesh

unread,

Dec 8, 2012, 5:17:48 PM12/8/12

to stp-...@googlegroups.com

You will have to use an IFF operator (if and only if operator) to
compare two Booleans.

-Vijay.