Merge pull request #1245 from diffblue/property_and1-fix

Fix for typechecking SVA `and` on named properties

Author: tautschnig

regression/verilog/SVA/property_and1.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 property_and1.sv
---bdd
+
+^\[.*\] always \(main\.P1 and main\.P1\): PROVED \(1-induction\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This is rejected with a typechecking error.

src/verilog/verilog_typecheck_sva.cpp

@@ -121,10 +121,8 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
     // These yield sequences when both operands are sequences, and
     // properties otherwise.
     if(
-      (expr.lhs().type().id() == ID_verilog_sva_sequence ||
-       !has_temporal_operator(expr.lhs())) &&
-      (expr.rhs().type().id() == ID_verilog_sva_sequence ||
-       !has_temporal_operator(expr.rhs())))
+      expr.lhs().type().id() != ID_verilog_sva_property &&
+      expr.rhs().type().id() != ID_verilog_sva_property)
     {
       expr.type() = verilog_sva_sequence_typet{};
       require_sva_sequence(expr.lhs());