X/Z bits in property mishandled by btor backend

[nakengelhardt]

Consider this example:

[options]
mode cover

[engines]
btor btormc

[script]
read -formal compare_x.sv
hierarchy -top compare_x
proc

[file compare_x.sv]
`define pat 	16'b100000????????01
module compare_x(input clk, input [15:0] a);
    always @(posedge clk) cover (a == `pat);
endmodule

According to standard a == comparison operation with a Z operand results in X output, so this is probably undefined behavior. Currently the smtbmc engine accepts this (I'm not sure if the result is what is intended in this code) but the btor engine produces an invalid btor file and crashes.
Can we do something to detect cases like this and error out with a meaningful message?