read_verilog <<EOT module top(input a, b, output o); wire tmp; assign o = tmp | 1'bx; assign tmp = a & 1'b0; endmodule EOT design -save read select -assert-count 1 t:$and select -assert-count 1 t:$or opt_expr select -assert-none t:$and t:$or sat -verify -enable_undef -prove o 1'bx design -load read opt_expr -keepdc select -assert-none t:$and t:$or sat -verify -enable_undef -prove o 1'bx design -load read simplemap opt_expr -keepdc select -assert-none t:$_AND_ t:$_OR_ sat -verify -enable_undef -prove o 1'bx design -load read simplemap opt_expr -keepdc select -assert-none t:$_AND_ t:$_OR_ sat -verify -enable_undef -prove o 1'bx