diff --git a/kernel/qcsat.cc b/kernel/qcsat.cc
index f996a963a..a5ecd5cb0 100644
--- a/kernel/qcsat.cc
+++ b/kernel/qcsat.cc
@@ -108,9 +108,17 @@ void SatEffortBudget::charge_import(QuickConeSat &qcsat, int64_t &cells_charged)
 	cells_charged = GetSize(qcsat.imported_cells);
 }
 
+SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &assumptions)
+{
+	std::vector<bool> modelVals;
+	return solve(qcsat, cap, {}, modelVals, assumptions);
+}
+
 SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &modelExprs,
 		std::vector<bool> &modelVals, const std::vector<int> &assumptions)
 {
+	if (spent())
+		return Result::LimitReached;
 	if (enabled())
 		cap = (cap > 0) ? std::min(cap, remaining) : remaining;
 	qcsat.ez->setSolverPropLimit(cap);
diff --git a/kernel/qcsat.h b/kernel/qcsat.h
index d0b717c8f..09d072f7c 100644
--- a/kernel/qcsat.h
+++ b/kernel/qcsat.h
@@ -102,6 +102,9 @@ struct SatEffortBudget {
 
 	Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &modelExprs,
 			std::vector<bool> &modelVals, const std::vector<int> &assumptions);
+
+	// Assumptions-only query without a model
+	Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &assumptions);
 };
 
 YOSYS_NAMESPACE_END