diff --git a/divine/smt/builder-smtlib.cpp b/divine/smt/builder-smtlib.cpp
index b4b9b4d0b551f60103ab78c2079412d8a25dc925..5d6c4c5433139b8fbc50f1776d48be2bf38bc072 100644
--- a/divine/smt/builder-smtlib.cpp
+++ b/divine/smt/builder-smtlib.cpp
@@ -241,7 +241,6 @@ SMTLib2::Node SMTLib2::binary( brq::smt_op op, Node a, Node b, int bw )
             case op_t::bool_or:
             case op_t::bv_or:
                 return define( _ctx.binop< op_t::bool_or >( 1, a, b ) );
-            case op_t::constraint:
             case op_t::bool_and:
             case op_t::bv_and:
                 return define( _ctx.binop< op_t::bool_and >( 1, a, b ) );
diff --git a/divine/smt/builder-stp.cpp b/divine/smt/builder-stp.cpp
index e84c6e286fad3104b85d58c49a972609910a0630..6679e244aac0c3b1df1ac540b7403df87336ceba 100644
--- a/divine/smt/builder-stp.cpp
+++ b/divine/smt/builder-stp.cpp
@@ -173,7 +173,6 @@ stp::ASTNode STP::binary( brq::smt_op op, Node a, Node b, int bw )
             case op_t::bool_or:
             case op_t::bv_or:
                 return _stp.CreateNode( stp::OR, a, b );
-            case op_t::constraint:
             case op_t::bool_and:
             case op_t::bv_and:
                 return _stp.CreateNode( stp::AND, a,  b );
diff --git a/divine/smt/builder-z3.cpp b/divine/smt/builder-z3.cpp
index c1a55e819ffd6bae9e81752f6a73b1c33901de98..5d33cf5d4e3ab951ce8133d6b786453530262aef 100644
--- a/divine/smt/builder-z3.cpp
+++ b/divine/smt/builder-z3.cpp
@@ -211,7 +211,6 @@ z3::expr Z3::binary( brq::smt_op op, Node a, Node b, int )
             case op_t::bv_or:
                 return a || b;
             case op_t::bool_and:
-            case op_t::constraint:
             case op_t::bv_and:
                 return a && b;
             case op_t::bv_uge:
diff --git a/divine/smt/rpn.hpp b/divine/smt/rpn.hpp
index 1285d7c42ab46a5a2f46000e7d736c297c0ab23e..a6b28f8ede8bcddac762137be1553467187189e8 100644
--- a/divine/smt/rpn.hpp
+++ b/divine/smt/rpn.hpp
@@ -30,7 +30,7 @@
 namespace divine::smt
 {
     template< typename builder_t, typename expr_t >
-    auto evaluate( builder_t &bld, const expr_t &expr, bool *is_constraint = nullptr )
+    auto evaluate( builder_t &bld, const expr_t &expr )
     {
         using node_t = typename builder_t::Node;
 
@@ -54,9 +54,6 @@ namespace divine::smt
 
         for ( auto &atom : expr )
         {
-            if ( is_constraint )
-                *is_constraint = atom.op == brq::smt_op::constraint;
-
             auto op = atom.op;
 
             if      ( atom.varid() )      push( bld.variable( atom.varid(), atom.bw() ), atom.bw() );