diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 87055431405..f79e434f08c 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -2313,16 +2313,14 @@ void java_bytecode_convert_methodt::convert_athrow(
     // we translate athrow into
     // ASSERT false;
     // ASSUME false:
-    code_assertt assert_code;
-    assert_code.assertion() = false_exprt();
+    code_assertt assert_code(false_exprt{});
     source_locationt assert_location = location; // copy
     assert_location.set_comment("assertion at " + location.as_string());
     assert_location.set("user-provided", true);
     assert_location.set_property_class(ID_assertion);
     assert_code.add_source_location() = assert_location;
 
-    code_assumet assume_code;
-    assume_code.assumption() = false_exprt();
+    code_assumet assume_code(false_exprt{});
     source_locationt assume_location = location; // copy
     assume_location.set("user-provided", true);
     assume_code.add_source_location() = assume_location;
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index e575f613d9c..b88201f8353 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -320,7 +320,7 @@ void shared_bufferst::write(
   target=goto_program.insert_before(target);
   target->guard=cond_expr;
   target->type=ASSERT;
-  target->code=code_assertt();
+  target->code = code_assertt(cond_expr);
   target->code.add_source_location()=source_location;
   target->source_location=source_location;
   target++;