@@ -783,14 +783,15 @@ static inline sva_and_exprt &to_sva_and_expr(exprt &expr)
783783 return static_cast <sva_and_exprt &>(expr);
784784}
785785
786- class sva_sequence_concatenation_exprt : public binary_predicate_exprt
786+ class sva_sequence_concatenation_exprt : public binary_exprt
787787{
788788public:
789789 explicit sva_sequence_concatenation_exprt (exprt op0, exprt op1)
790- : binary_predicate_exprt (
790+ : binary_exprt (
791791 std::move (op0),
792792 ID_sva_sequence_concatenation,
793- std::move(op1))
793+ std::move(op1),
794+ verilog_sva_sequence_typet{})
794795 {
795796 }
796797};
@@ -925,7 +926,7 @@ class sva_cycle_delay_exprt : public ternary_exprt
925926 std::move (from),
926927 std::move(to),
927928 std::move(op),
928- bool_typet() )
929+ verilog_sva_sequence_typet{} )
929930 {
930931 }
931932
@@ -935,7 +936,7 @@ class sva_cycle_delay_exprt : public ternary_exprt
935936 std::move (cycles),
936937 nil_exprt{},
937938 std::move (op),
938- bool_typet() )
939+ verilog_sva_sequence_typet{} )
939940 {
940941 }
941942
@@ -1001,7 +1002,10 @@ class sva_cycle_delay_plus_exprt : public unary_exprt
10011002{
10021003public:
10031004 explicit sva_cycle_delay_plus_exprt (exprt op)
1004- : unary_exprt(ID_sva_cycle_delay_plus, std::move(op), bool_typet())
1005+ : unary_exprt(
1006+ ID_sva_cycle_delay_plus,
1007+ std::move (op),
1008+ verilog_sva_sequence_typet{})
10051009 {
10061010 }
10071011};
@@ -1026,7 +1030,10 @@ class sva_cycle_delay_star_exprt : public unary_exprt
10261030{
10271031public:
10281032 explicit sva_cycle_delay_star_exprt (exprt op)
1029- : unary_exprt(ID_sva_cycle_delay_star, std::move(op), bool_typet())
1033+ : unary_exprt(
1034+ ID_sva_cycle_delay_star,
1035+ std::move (op),
1036+ verilog_sva_sequence_typet{})
10301037 {
10311038 }
10321039};
@@ -1372,7 +1379,7 @@ class sva_sequence_goto_repetition_exprt : public binary_exprt
13721379 std::move (__op),
13731380 ID_sva_sequence_goto_repetition,
13741381 std::move (__repetitions),
1375- bool_typet {}}
1382+ verilog_sva_sequence_typet {}}
13761383 {
13771384 }
13781385
@@ -1428,7 +1435,7 @@ class sva_sequence_non_consecutive_repetition_exprt : public binary_exprt
14281435 std::move (__op),
14291436 ID_sva_sequence_non_consecutive_repetition,
14301437 std::move (__repetitions),
1431- bool_typet {}}
1438+ verilog_sva_sequence_typet {}}
14321439 {
14331440 }
14341441
0 commit comments