Failed assertion when using vc_boolType

[Stephan Falke]

Hi,

vc_boolType fails with assertion in NonMemberBVConstEvaluator
(consteval.cpp, failing assertion is in line 41). This method should
probably not be called in this case. The following patch seems to fix
the problem, but I am not sure whether this is the "right" fix.

Best regards,
Stephan


Index: src/AST/NodeFactory/SimplifyingNodeFactory.cpp
===================================================================
--- src/AST/NodeFactory/SimplifyingNodeFactory.cpp (revision 1398)
+++ src/AST/NodeFactory/SimplifyingNodeFactory.cpp (working copy)
@@ -39,7 +39,7 @@

// If all the parameters are constant, return the constant value.
// The bitblaster calls CreateNode with a boolean vector. We don't
try to simplify those.
- if (kind != BEEV::UNDEFINED && kind != BEEV::BITVECTOR && kind !=
BEEV::ARRAY)
+ if (kind != BEEV::UNDEFINED && kind != BEEV::BOOLEAN && kind !=
BEEV::BITVECTOR && kind != BEEV::ARRAY)
{
bool allConstant = true;

[Trevor Hansen]

Hi Stephan, Thanks for the fix! It's applied in revision 1400.

Trevor.