diff --git a/regression/verilog/expressions/minus1.desc b/regression/verilog/expressions/minus1.desc
index 9ba0a4de5..51fdb1242 100644
--- a/regression/verilog/expressions/minus1.desc
+++ b/regression/verilog/expressions/minus1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 minus1.sv
 
 ^EXIT=0$
@@ -6,4 +6,3 @@ minus1.sv
 --
 ^warning: ignoring
 --
-The result is wrong.
diff --git a/regression/verilog/expressions/mult1.desc b/regression/verilog/expressions/mult1.desc
index 66625f656..57e745ac6 100644
--- a/regression/verilog/expressions/mult1.desc
+++ b/regression/verilog/expressions/mult1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 mult1.sv
 
 ^EXIT=0$
@@ -6,4 +6,3 @@ mult1.sv
 --
 ^warning: ignoring
 --
-The result is wrong.
diff --git a/regression/verilog/expressions/plus1.desc b/regression/verilog/expressions/plus1.desc
index 992ec7513..73ad5068d 100644
--- a/regression/verilog/expressions/plus1.desc
+++ b/regression/verilog/expressions/plus1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 plus1.sv
 
 ^EXIT=0$
@@ -6,4 +6,3 @@ plus1.sv
 --
 ^warning: ignoring
 --
-The result is wrong.
diff --git a/regression/verilog/expressions/unary_minus1.desc b/regression/verilog/expressions/unary_minus1.desc
index 5eda7e47d..fb08c62ad 100644
--- a/regression/verilog/expressions/unary_minus1.desc
+++ b/regression/verilog/expressions/unary_minus1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 unary_minus1.sv
 
 ^EXIT=0$
@@ -6,4 +6,3 @@ unary_minus1.sv
 --
 ^warning: ignoring
 --
-The result is wrong.
diff --git a/src/verilog/aval_bval_encoding.cpp b/src/verilog/aval_bval_encoding.cpp
index 78167552c..426906150 100644
--- a/src/verilog/aval_bval_encoding.cpp
+++ b/src/verilog/aval_bval_encoding.cpp
@@ -36,8 +36,7 @@ bv_typet aval_bval_type(std::size_t width, irep_idt source_type)
 
 bv_typet lower_to_aval_bval(const typet &src)
 {
-  PRECONDITION(
-    src.id() == ID_verilog_unsignedbv || src.id() == ID_verilog_signedbv);
+  PRECONDITION(is_four_valued(src));
   return aval_bval_type(to_bitvector_type(src).get_width(), src.id());
 }
 
@@ -75,9 +74,7 @@ typet aval_bval_underlying(const typet &src)
 
 constant_exprt lower_to_aval_bval(const constant_exprt &src)
 {
-  PRECONDITION(
-    src.type().id() == ID_verilog_signedbv ||
-    src.type().id() == ID_verilog_unsignedbv);
+  PRECONDITION(is_four_valued(src.type()));
 
   auto new_type = lower_to_aval_bval(src.type());
   auto width = aval_bval_width(new_type);
@@ -256,7 +253,7 @@ exprt has_xz(const exprt &expr)
     return false_exprt{}; // it's two-valued
 }
 
-/// return 'x', one bit, in aval_bval encoding
+/// return 'x'
 exprt make_x(const typet &type)
 {
   PRECONDITION(is_four_valued(type));
@@ -470,3 +467,33 @@ exprt aval_bval(const shift_exprt &expr)
   auto x = make_x(expr.type());
   return if_exprt{distance_has_xz, x, combined};
 }
+
+exprt default_aval_bval_lowering(const exprt &expr)
+{
+  auto &type = expr.type();
+
+  PRECONDITION(is_four_valued(type));
+
+  exprt::operandst disjuncts;
+  for(auto &op : expr.operands())
+    disjuncts.push_back(has_xz(op));
+
+  auto has_xz = disjunction(disjuncts);
+
+  exprt two_valued_expr = expr; // copy
+
+  for(auto &op : two_valued_expr.operands())
+    op = aval_underlying(op); // replace by aval
+
+  if(type.id() == ID_verilog_unsignedbv)
+    two_valued_expr.type() = unsignedbv_typet{to_bitvector_type(type).width()};
+  else if(type.id() == ID_verilog_signedbv)
+    two_valued_expr.type() = signedbv_typet{to_bitvector_type(type).width()};
+  else
+    PRECONDITION(false);
+
+  return if_exprt{
+    has_xz,
+    make_x(type),
+    aval_bval_conversion(two_valued_expr, lower_to_aval_bval(type))};
+}
diff --git a/src/verilog/aval_bval_encoding.h b/src/verilog/aval_bval_encoding.h
index 5b29d238a..cf8720a4c 100644
--- a/src/verilog/aval_bval_encoding.h
+++ b/src/verilog/aval_bval_encoding.h
@@ -66,4 +66,9 @@ exprt aval_bval(const typecast_exprt &);
 /// lowering for shifts
 exprt aval_bval(const shift_exprt &);
 
+/// If any operand has x/z, then the result is 'x'.
+/// Otherwise, the result is the expression applied to the aval
+/// of the operands.
+exprt default_aval_bval_lowering(const exprt &);
+
 #endif
diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 3da22d8a6..88a2bcbfa 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -614,9 +614,23 @@ exprt verilog_lowering(exprt expr)
     {
       // turn into floatbv
       expr.type() = verilog_lowering(expr.type());
+      return expr;
     }
-
-    return expr;
+    else if(is_four_valued(expr))
+    {
+      return default_aval_bval_lowering(expr);
+    }
+    else
+      return expr;
+  }
+  else if(
+    expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
+    expr.id() == ID_div || expr.id() == ID_mod)
+  {
+    if(is_four_valued(expr))
+      return default_aval_bval_lowering(expr);
+    else
+      return expr;
   }
   else if(expr.id() == ID_lshr || expr.id() == ID_ashr || expr.id() == ID_shl)
   {