In reply to Reuben:
The property gets attempted on each clock cycle. If a is low, the the else block is taken and the property sig1 & sig2 & sig3 → ##1 sig_B is evaluated. Since sig3 is low, the whole antecedent is false. For implication, a false antecedent is a vacuous pass. Since the property under the else evaluated to pass, the whole if/else property evaluates to pass. I couldn’t find the vacuity semantics for if/else explicitly written out int he LRM, but I presume that they are similar to those for implication. This means that, since the evaluation of the property under the else was vacuous, then the entire evaluation of the if/else is also vacuous.
Also, I noticed that you were also asking how to have the tool not mark the assertion as passed. You can only do this with a disable iff. I’m not sure what the best practices w.r.t. using this are, but you for sure want to use $sampled(…) inside it due to the way the semantics are defined. I guess in your case it would look something like:
property my_property;
disable iff ($sampled(!a && !(sig1 & sig2 & sig3)))
// ...
endproperty
The issue with vacuity you will have regardless of whether you split your assertion into two smaller assertions or not. Tools usually either don’t collect vacuous passes by default or if they do they categorize them separately.