#include #include #ifdef __divine__ #include #else #include #endif using namespace abstract; extern "C" { bool __tristate_lower( Tristate tristate ) _ROOT { if ( tristate.value == Tristate::Value::Unknown ) { #ifdef __divine__ return __vm_choose( 2 ); #else return std::rand() % 2; #endif } return tristate.value; } Tristate __tristate_lift( bool v ) _ROOT { return v ? Tristate::Value::True : Tristate::Value::False; } }