diff --git a/kernel/bitsim.h b/kernel/bitsim.h
index a0915e28b..c659a5e34 100644
--- a/kernel/bitsim.h
+++ b/kernel/bitsim.h
@@ -15,10 +15,10 @@ struct BitSim {
 	BitSim(Module *m, SigMap &sm, ModWalker &mw) 
 		: module(m), sigmap(sm), modwalker(mw), rng_state(1337) {}
 
-	uint64_t xorshift64() {
-		rng_state ^= rng_state << 13;
-		rng_state ^= rng_state >> 7;
-		rng_state ^= rng_state << 17;
+	uint64_t next_rand() {
+		uint32_t lo = mkhash_xorshift((uint32_t)rng_state);
+		uint32_t hi = mkhash_xorshift((uint32_t)(rng_state >> 32) ^ lo);
+		rng_state = ((uint64_t)hi << 32) | lo;
 		return rng_state;
 	}
 
@@ -34,17 +34,17 @@ struct BitSim {
 		uint64_t res = 0;
 
 		if (!modwalker.has_drivers(mapped)) {
-			res = xorshift64();
+			res = next_rand();
 		} else {
 			auto &drivers = modwalker.signal_drivers[mapped];
 			if (drivers.empty()) {
-				res = xorshift64();
+				res = next_rand();
 			} else {
 				auto driver = *drivers.begin();
 				Cell *cell = driver.cell;
 				
 				if (cell->is_builtin_ff()) {
-					res = xorshift64();
+					res = next_rand();
 				} else if (cell->type == ID($_AND_)) {
 					res = eval_bit(cell->getPort(ID::A)[0]) & eval_bit(cell->getPort(ID::B)[0]);
 				} else if (cell->type == ID($_OR_)) {
@@ -64,7 +64,7 @@ struct BitSim {
 					uint64_t b = eval_bit(cell->getPort(ID::B)[driver.offset]);
 					res = (a & ~s) | (b & s);
 				} else {
-					res = xorshift64();
+					res = next_rand();
 				}
 			}
 		}
diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc
index 500df142e..6984f3f4b 100644
--- a/passes/opt/opt_dff.cc
+++ b/passes/opt/opt_dff.cc
@@ -968,14 +968,6 @@ struct OptDffWorker
 		return s == State::S0 || s == State::S1;
 	}
 
-	int sat_mux(QuickConeSat &qcsat, int s, int a, int b) {
-		return qcsat.ez->OR(qcsat.ez->AND(s, a), qcsat.ez->AND(qcsat.ez->NOT(s), b));
-	}
-
-	int sat_const(QuickConeSat &qcsat, State v) {
-		return v == State::S1 ? qcsat.ez->CONST_TRUE : qcsat.ez->CONST_FALSE;
-	}
-
 	std::vector<std::vector<int>> gather_initial_eq_classes(std::vector<EqBit> &bits, dict<Cell *, FfData> &ff_for_cell)
 	{
 		std::vector<SigKey> keys;
@@ -1065,7 +1057,7 @@ struct OptDffWorker
 
 		// Assume same class
 		for (auto &cls : classes) {
-			uint64_t class_q_val = sim.xorshift64();
+			uint64_t class_q_val = sim.next_rand();
 			for (int idx : cls) {
 				sim.sim_vals[sigmap(bits[idx].q)] = class_q_val;
 			}
@@ -1137,12 +1129,12 @@ struct OptDffWorker
 				if (ff.has_aload) {
 					int al = qcsat.importSigBit(ff.sig_aload);
 					if (!ff.pol_aload) al = qcsat.ez->NOT(al);
-					n = sat_mux(qcsat, al, qcsat.importSigBit(ff.sig_ad[eb.idx]), n);
+					n = qcsat.ez->ITE(al, qcsat.importSigBit(ff.sig_ad[eb.idx]), n);
 				}
 				if (ff.has_arst) {
 					int ar = qcsat.importSigBit(ff.sig_arst);
 					if (!ff.pol_arst) ar = qcsat.ez->NOT(ar);
-					n = sat_mux(qcsat, ar, sat_const(qcsat, ff.val_arst[eb.idx]), n);
+					n = qcsat.ez->ITE(ar, qcsat.ez->value(ff.val_arst[eb.idx] == State::S1), n);
 				}
 				if (ff.has_sr) {
 					int clr = qcsat.importSigBit(ff.sig_clr[eb.idx]);
@@ -1154,7 +1146,7 @@ struct OptDffWorker
 				if (ff.has_srst) {
 					int srst = qcsat.importSigBit(ff.sig_srst);
 					if (!ff.pol_srst) srst = qcsat.ez->NOT(srst);
-					n = sat_mux(qcsat, srst, sat_const(qcsat, ff.val_srst[eb.idx]), n);
+					n = qcsat.ez->ITE(srst, qcsat.ez->value(ff.val_srst[eb.idx] == State::S1), n);
 				}
 
 				n_lit[idx] = n;
@@ -1191,7 +1183,8 @@ struct OptDffWorker
 				if (n_lit[rep] == n_lit[cls[i]])
 					continue;
 
-				int query = qcsat.ez->NOT(qcsat.ez->IFF(n_lit[rep], n_lit[cls[i]]));
+				// next-state bits differ
+				int query = qcsat.ez->XOR(n_lit[rep], n_lit[cls[i]]);
 				std::vector<int> modelExprs;
 				for (int b : cls)
 					modelExprs.push_back(n_lit[b]);