diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index e00becc56e9..2853fd4e50b 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -1578,7 +1578,7 @@ void smt2_convt::convert_expr(const exprt &expr)
       if(expr.id() == ID_nand)
         out << "(and";
       else if(expr.id() == ID_nor)
-        out << "(and";
+        out << "(or";
       else if(expr.id() == ID_xnor)
         out << "(xor";
       else
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 9ee74ba1dad..75c3d3c004e 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -2103,7 +2103,7 @@ inline and_exprt &to_and_expr(exprt &expr)
 /// Any number of operands that is greater or equal one.
 /// When given one operand, this is equivalent to the negation.
 /// When given three or more operands, this is equivalent to the negation
-/// of the and expression with the same operands.
+/// of the 'and' expression with the same operands.
 class nand_exprt : public multi_ary_exprt
 {
 public:
@@ -2248,7 +2248,7 @@ inline or_exprt &to_or_expr(exprt &expr)
 /// Any number of operands that is greater or equal one.
 /// When given one operand, this is equivalent to the negation.
 /// When given three or more operands, this is equivalent to the negation
-/// of the and expression with the same operands.
+/// of the 'or' expression with the same operands.
 class nor_exprt : public multi_ary_exprt
 {
 public:
@@ -2331,7 +2331,7 @@ inline xor_exprt &to_xor_expr(exprt &expr)
 ///
 /// When given one operand, this is equivalent to the negation.
 /// When given three or more operands, this is equivalent to the negation
-/// of the xor expression with the same operands.
+/// of the 'xor' expression with the same operands.
 class xnor_exprt : public multi_ary_exprt
 {
 public: