diff --git a/docs/systemverilog/README.md b/docs/systemverilog/README.md
index b17cfe4f..f06fb373 100644
--- a/docs/systemverilog/README.md
+++ b/docs/systemverilog/README.md
@@ -58,6 +58,37 @@ build/src/bin/kepler-formal -sv2v -v sec \
 
 The preprocessing flag is spelled `--verilog_preprocessing`.
 
+## Initial values
+
+The slang frontend lowers constant register initialization to DFF `INIT`
+metadata, and SEC extraction adopts it as an exact initial-state constraint:
+
+- `initial q = 1'b0;` — an initial block holding a single blocking constant
+  assignment to a register
+- `logic q = 1'b0;` — a declaration initializer (semantically an implicit
+  initial block)
+
+`x`/`z` digits leave the corresponding state bit unconstrained. Registers
+without an explicit initializer keep a free initial state, so designs that
+initialize state through a reset sequence still need
+[sec-reset-bootstrap](../sec-reset-bootstrap.md).
+
+Sized bit-literal parameters (such as `INIT`) are stored in SNL in a canonical
+form — `<width>'b<msb...lsb>` with lowercase `0`/`1`/`x`/`z` digits — produced
+by the naja frontends at load time. SEC extraction only consumes this canonical
+form; any other string form leaves the state unconstrained.
+
+Limitations:
+
+- Initial blocks with multiple statements, non-blocking assignments, or
+  non-constant right-hand sides are rejected by the frontend at load time.
+- Memory initialization (`$readmemh`/`$readmemb`, memory `INIT` parameters) is
+  not adopted by SEC extraction yet.
+- The `-verilog` flow uses a structural Verilog parser and does not process
+  initial blocks; use `-systemverilog`/`-sv` for designs that rely on them.
+  In `-sv2v` comparisons, design 1 is parsed by the slang frontend and supports
+  these initializers, while design 2 (Verilog) does not.
+
 ## Flist mode
 
 For SystemVerilog designs that are already driven by a slang command file or flist, use:
diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 2b7a4d47..ade76579 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -27,7 +27,11 @@
 #include "NLDB0.h"
 #include "NLName.h"
 #include "NLUniverse.h"
+#include "SNLBusTerm.h"
+#include "SNLBusTermBit.h"
 #include "SNLDesignModeling.h"
+#include "SNLInstParameter.h"
+#include "SNLInstance.h"
 #include "SNLPath.h"
 #include "../../clauses/SNLLogicCloud.h"
 #include "../../clauses/Tree2BoolExpr.h"
@@ -3157,6 +3161,84 @@ void appendPendingTransitionsForInstance(
   }
 }
 
+// Reads the canonical INIT digit ("<width>'b<msb...lsb>", lowercase 0/1/x/z)
+// for the given state output terminal, in the storage element's own polarity.
+// The naja frontends always store INIT in this form with the width of the Q
+// output; anything else is treated as absent and leaves the state
+// unconstrained.
+std::optional<bool> readDFFInitDigitForStateTerm(
+    const naja::DNL::DNLTerminalFull& term) {
+  if (term.isNull() || term.isTopPort()) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  const auto* snlInstance = term.getDNLInstance().getSNLInstance();
+  if (snlInstance == nullptr) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  const auto* initParam =
+      snlInstance->getInstParameter(naja::NL::NLName("INIT"));
+  if (initParam == nullptr) {
+    return std::nullopt;
+  }
+  const std::string value = initParam->getValue();
+  const auto basePos = value.find('\'');
+  if (basePos == std::string::npos || basePos + 2 >= value.size() ||
+      (value[basePos + 1] != 'b' && value[basePos + 1] != 'B')) {
+    return std::nullopt;  // non-canonical INIT
+  }
+  const size_t width = value.size() - (basePos + 2);
+  size_t digitIndex = 0;  // into the MSB-first digit string
+  if (const auto* busBit =
+          dynamic_cast<const naja::NL::SNLBusTermBit*>(term.getSnlBitTerm())) {
+    const auto* bus = busBit->getBus();
+    if (width != static_cast<size_t>(bus->getWidth())) {
+      return std::nullopt;  // INIT width must match the Q output width
+    }
+    // Digit 0 of the canonical form is the bus MSB, for either ascending or
+    // descending ranges.
+    const auto msb = bus->getMSB();
+    const auto bit = busBit->getBit();
+    digitIndex = static_cast<size_t>(msb >= bit ? msb - bit : bit - msb);
+  } else if (width != 1) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  switch (std::tolower(static_cast<unsigned char>(value[basePos + 2 + digitIndex]))) {
+    case '0':
+      return false;
+    case '1':
+      return true;
+    default:
+      return std::nullopt;  // x/z leave the state unconstrained
+  }
+}
+
+// Transfers DFF INIT metadata onto the extracted model. Each state key holds
+// values in its own observed pin polarity: the primary key follows
+// stateOutputIsComplemented (mirroring the next-state build) and complemented
+// keys get the opposite value.
+void harvestInitialStateValues(ExtractContext& ctx, SequentialDesignModel& model) {
+  size_t harvested = 0;
+  for (const auto& pending : ctx.pendingTransitions) {
+    const auto& term = ctx.dnl->getDNLTerminalFromID(pending.stateTermID);
+    const auto digit = readDFFInitDigitForStateTerm(term);
+    if (!digit.has_value()) {
+      continue;
+    }
+    const bool value = pending.stateOutputIsComplemented ? !*digit : *digit;
+    model.initialStateValueByKey.emplace(pending.stateKey, value);
+    for (const auto& complementedKey : pending.complementedStateKeys) {
+      model.initialStateValueByKey.emplace(complementedKey, !value);
+    }
+    ++harvested;
+  }
+  if (ctx.secDiagEnabled && harvested > 0) {
+    fprintf(stderr,
+            "SEC diag: extract(%s) harvested initial state values=%zu\n",
+            ctx.topName.c_str(), harvested);
+    fflush(stderr);
+  }
+}
+
 void collectSequentialTransitions(ExtractContext& ctx, SequentialDesignModel& model) {
   // Record enough pin information to reconstruct Q' after the combinational
   // Boolean expressions have been built.
@@ -3179,6 +3261,7 @@ void collectSequentialTransitions(ExtractContext& ctx, SequentialDesignModel& mo
     }
     appendPendingTransitionsForInstance(ctx, model, *scan);
   }
+  harvestInitialStateValues(ctx, model);
 }
 
 std::vector<naja::DNL::DNLID> collectInitialObservedTerms(const ExtractContext& ctx) {
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index 08e4f6e9..a10f4d85 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -37,6 +37,8 @@
 #include "SNLBusTerm.h"
 #include "SNLBusTermBit.h"
 #include "SNLInstance.h"
+#include "SNLInstParameter.h"
+#include "SNLParameter.h"
 #include "SNLScalarNet.h"
 #include "SNLScalarTerm.h"
 #include "common/AlignedSignals.h"
@@ -15896,6 +15898,342 @@ TEST_F(SequentialEquivalenceStrategyTests,
   EXPECT_TRUE(model.initialStateValueByKey.empty());
 }
 
+SNLDesign* createWideDffTopWithInit(
+    NLLibrary* library,
+    const std::string& name,
+    const char* initValue) {
+  auto* top =
+      SNLDesign::create(library, SNLDesign::Type::Standard, NLName(name));
+  auto* topIn = SNLBusTerm::create(
+      top, SNLTerm::Direction::Input, 3, 0, NLName("in"));
+  auto* topClock = SNLScalarTerm::create(
+      top, SNLTerm::Direction::Input, NLName("clk"));
+  auto* topOut = SNLBusTerm::create(
+      top, SNLTerm::Direction::Output, 3, 0, NLName("out"));
+
+  auto* dffModel = NLDB0::getOrCreateDFF(4);
+  auto* ff = SNLInstance::create(top, dffModel, NLName("ff0"));
+  auto* netIn = SNLBusNet::create(top, 3, 0, NLName("net_in"));
+  auto* netClock = SNLScalarNet::create(top, NLName("net_clk"));
+  auto* netQ = SNLBusNet::create(top, 3, 0, NLName("net_q"));
+
+  auto* dataTerm = dffModel->getBusTerm(NLName("D"));
+  auto* outputTerm = dffModel->getBusTerm(NLName("Q"));
+  topClock->setNet(netClock);
+  ff->getInstTerm(dffModel->getScalarTerm(NLName("C")))->setNet(netClock);
+  for (int bit = 0; bit <= 3; ++bit) {
+    topIn->getBit(bit)->setNet(netIn->getBit(bit));
+    ff->getInstTerm(dataTerm->getBit(bit))->setNet(netIn->getBit(bit));
+    ff->getInstTerm(outputTerm->getBit(bit))->setNet(netQ->getBit(bit));
+    topOut->getBit(bit)->setNet(netQ->getBit(bit));
+  }
+  SNLInstParameter::create(
+      ff, dffModel->getParameter(NLName("INIT")), initValue);
+  return top;
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsDFFInitParameter) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* invModel = createInvModel(primitives);
+  auto* top = createDffTop(library, "top", invModel, false, false);
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  auto* initParam = ff->getModel()->getParameter(NLName("INIT"));
+  ASSERT_NE(initParam, nullptr);
+  SNLInstParameter::create(ff, initParam, "1'b1");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 1u);
+  EXPECT_TRUE(extracted.initialStateValueByKey.begin()->second);
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsDFFInitParameterZero) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* invModel = createInvModel(primitives);
+  auto* top = createDffTop(library, "top", invModel, false, false);
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  auto* initParam = ff->getModel()->getParameter(NLName("INIT"));
+  ASSERT_NE(initParam, nullptr);
+  SNLInstParameter::create(ff, initParam, "1'b0");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 1u);
+  EXPECT_FALSE(extracted.initialStateValueByKey.begin()->second);
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractLeavesUnknownDFFInitUnconstrained) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* invModel = createInvModel(primitives);
+  auto* top = createDffTop(library, "top", invModel, false, false);
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  auto* initParam = ff->getModel()->getParameter(NLName("INIT"));
+  ASSERT_NE(initParam, nullptr);
+  // An explicit all-x INIT (the NLDB0 default) must not constrain the state.
+  SNLInstParameter::create(ff, initParam, "1'bx");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  EXPECT_TRUE(extracted.initialStateValueByKey.empty());
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsWideDFFInitParameter) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  // INIT digits are MSB first: bit3=0, bit2=1, bit1=x (unconstrained), bit0=0.
+  auto* top = createWideDffTopWithInit(library, "top", "4'b01x0");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.stateBits.size(), 4u);
+  EXPECT_EQ(extracted.initialStateValueByKey.size(), 3u);
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[3]")));
+  EXPECT_TRUE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[2]")));
+  EXPECT_EQ(
+      extracted.initialStateValueByKey.find(
+          findKeyByDisplayName(extracted, "ff0.Q[1]")),
+      extracted.initialStateValueByKey.end());
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[0]")));
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsAscendingBusDFFInitParameter) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+
+  // A flip-flop primitive with ascending D/Q buses [0:3].
+  auto* model = SNLDesign::create(
+      primitives, SNLDesign::Type::Primitive, NLName("DFF_ASC"));
+  auto* clock =
+      SNLScalarTerm::create(model, SNLTerm::Direction::Input, NLName("C"));
+  auto* data =
+      SNLBusTerm::create(model, SNLTerm::Direction::Input, 0, 3, NLName("D"));
+  auto* output =
+      SNLBusTerm::create(model, SNLTerm::Direction::Output, 0, 3, NLName("Q"));
+  SNLParameter::create(
+      model, NLName("INIT"), SNLParameter::Type::Binary, "4'bxxxx");
+  SNLDesignModeling::BitTerms outputBits;
+  SNLDesignModeling::BitTerms dataBits;
+  for (int bit = 0; bit <= 3; ++bit) {
+    outputBits.push_back(output->getBit(bit));
+    dataBits.push_back(data->getBit(bit));
+  }
+  SNLDesignModeling::addClockToOutputsArcs(clock, outputBits);
+  SNLDesignModeling::addInputsToClockArcs(dataBits, clock);
+  SNLDesignModeling::SequentialModel sequentialModel;
+  sequentialModel.kind = SNLDesignModeling::SequentialModel::Kind::FlipFlop;
+  sequentialModel.clockedOn = makeSequentialTermExpression(clock);
+  for (int bit = 0; bit <= 3; ++bit) {
+    SNLDesignModeling::SequentialState state;
+    state.nextState = makeSequentialTermExpression(data->getBit(bit));
+    sequentialModel.states.push_back(std::move(state));
+    sequentialModel.outputs.push_back(
+        {output->getBit(bit), makeSequentialStateExpression(bit)});
+  }
+  SNLDesignModeling::setSequentialModel(model, sequentialModel);
+
+  auto* top =
+      SNLDesign::create(library, SNLDesign::Type::Standard, NLName("top"));
+  auto* topIn = SNLBusTerm::create(
+      top, SNLTerm::Direction::Input, 0, 3, NLName("in"));
+  auto* topClock = SNLScalarTerm::create(
+      top, SNLTerm::Direction::Input, NLName("clk"));
+  auto* topOut = SNLBusTerm::create(
+      top, SNLTerm::Direction::Output, 0, 3, NLName("out"));
+  auto* ff = SNLInstance::create(top, model, NLName("ff0"));
+  auto* netIn = SNLBusNet::create(top, 0, 3, NLName("net_in"));
+  auto* netClock = SNLScalarNet::create(top, NLName("net_clk"));
+  auto* netQ = SNLBusNet::create(top, 0, 3, NLName("net_q"));
+  topClock->setNet(netClock);
+  ff->getInstTerm(model->getScalarTerm(NLName("C")))->setNet(netClock);
+  for (int bit = 0; bit <= 3; ++bit) {
+    topIn->getBit(bit)->setNet(netIn->getBit(bit));
+    ff->getInstTerm(data->getBit(bit))->setNet(netIn->getBit(bit));
+    ff->getInstTerm(output->getBit(bit))->setNet(netQ->getBit(bit));
+    topOut->getBit(bit)->setNet(netQ->getBit(bit));
+  }
+  // Canonical digit 0 is the declared leftmost index (bit 0 for [0:3]).
+  SNLInstParameter::create(
+      ff, model->getParameter(NLName("INIT")), "4'b01x0");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.stateBits.size(), 4u);
+  EXPECT_EQ(extracted.initialStateValueByKey.size(), 3u);
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[0]")));
+  EXPECT_TRUE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[1]")));
+  EXPECT_EQ(
+      extracted.initialStateValueByKey.find(
+          findKeyByDisplayName(extracted, "ff0.Q[2]")),
+      extracted.initialStateValueByKey.end());
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[3]")));
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractIgnoresNonCanonicalDFFInit) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* invModel = createInvModel(primitives);
+  auto* top = createDffTop(library, "top", invModel, false, false);
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  auto* initParam = ff->getModel()->getParameter(NLName("INIT"));
+  ASSERT_NE(initParam, nullptr);
+  // Only the canonical sized-binary form (written by the naja frontends) is
+  // harvested; anything else leaves the state unconstrained.
+  SNLInstParameter::create(ff, initParam, "1'h1");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  EXPECT_TRUE(extracted.initialStateValueByKey.empty());
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractIgnoresWidthMismatchedDFFInit) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  // The canonical form always covers the whole Q output; a width-mismatched
+  // INIT did not come from a naja frontend and leaves the state unconstrained.
+  auto* top = createWideDffTopWithInit(library, "top", "2'b11");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  EXPECT_TRUE(extracted.initialStateValueByKey.empty());
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsComplementedDFFInitParameter) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* model = createNamedComplementSequentialModel(
+      primitives, "DFF_Q_QN_INIT", "Q", "QN");
+  SNLParameter::create(
+      model, NLName("INIT"), SNLParameter::Type::Binary, "1'bx");
+  auto* top = createSequentialOutputPairTop(library, "top", model, "Q", "QN");
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  SNLInstParameter::create(
+      ff, model->getParameter(NLName("INIT")), "1'b1");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.complementedStateRelations.size(), 1u);
+  // State keys hold values in their own pin polarity: the Q key stores the
+  // INIT digit, the QN key stores its complement.
+  const auto primaryKey = findKeyByDisplayName(extracted, "ff0.Q[0]");
+  const auto complementKey = findKeyByDisplayName(extracted, "ff0.QN[0]");
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 2u);
+  EXPECT_TRUE(extracted.initialStateValueByKey.at(primaryKey));
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(complementKey));
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsSlangInitialBlock) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* top = loadSystemVerilogTopFromSource(
+      library,
+      "sec_slang_initial_block",
+      R"(module sec_slang_initial_block(
+  input  logic clk,
+  input  logic d,
+  output logic q
+);
+  logic r;
+  initial r = 1'b1;
+  always_ff @(posedge clk) r <= d;
+  assign q = r;
+endmodule
+)");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 1u);
+  EXPECT_TRUE(extracted.initialStateValueByKey.begin()->second);
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsSlangDeclarationInitializer) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* top = loadSystemVerilogTopFromSource(
+      library,
+      "sec_slang_decl_init",
+      R"(module sec_slang_decl_init(
+  input  logic clk,
+  input  logic d,
+  output logic q
+);
+  logic r = 1'b0;
+  always_ff @(posedge clk) r <= d;
+  assign q = r;
+endmodule
+)");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 1u);
+  EXPECT_FALSE(extracted.initialStateValueByKey.begin()->second);
+}
+
 TEST_F(SequentialEquivalenceStrategyTests,
        SequentialDesignModelExtractSupportsGenericComplementedStateNames) {
   NLUniverse::create();
diff --git a/thirdparty/naja b/thirdparty/naja
index ad34893b..1bc68280 160000
--- a/thirdparty/naja
+++ b/thirdparty/naja
@@ -1 +1 @@
-Subproject commit ad34893beb810ce4e30af9b5f82a7612c8be6992
+Subproject commit 1bc682800ea6175b15977492f80e90b69d0a826f