nfa: +fix Build the product map in naive inclusion only for a counterexample

[Adda0]

is_included_naive() always passed &prod_map to intersection(), but it
only reads the map to translate the counterexample path back to smaller's
states. Without a counterexample the map is filled and thrown away.

Measured on a 600 000-state / 3 591 612-transition product (Release
-O3 -DNDEBUG, GCC 16.2, pinned to one core, 3 runs): intersection() takes
536-574 ms with the map and 218-297 ms without it.

Part of #750.
Part of #726.

[greptile-apps]

Confidence Score: 5/5

[Medium risk] Optimizes product map construction in inclusion check.

The PR appears safe to merge; it skips an unused map without changing inclusion results or counterexample paths.

What we checked:

• Inclusion without a counterexample: product_storage tracks product states independently. Writes to product_map check for null, and is_included_naive() only reads the map when cex is non-null.

Summary

is_included_naive() now asks intersection() to fill prod_map only when the caller requests a counterexample.

• Avoids unused map entries when cex is null.
• Keeps counterexample path translation unchanged.
• No actionable issues found.

_{Reviews (1) · Last reviewed commit: 0351789 · Reviewed by Greptile}