clause stuff

toolCHAINZ · toolCHAINZ · commit fea1e2d19d0d · 2025-01-01T14:42:32.000Z
diff --git a/src/synthesis/pcode_theory/theory_constraint.rs b/src/synthesis/pcode_theory/theory_constraint.rs
@@ -47,6 +47,11 @@ pub(crate) fn gen_conflict_clauses(
     if result.is_empty() {
         None
     } else {
-        Some(ConflictClause::combine(result.as_slice()))
+        let c = ConflictClause::combine(result.as_slice());
+        if c.decisions().is_empty() {
+            None
+        } else {
+            Some(c)
+        }
     }
 }

Original file line number	Diff line number	Diff line change
`@@ -47,6 +47,11 @@ pub(crate) fn gen_conflict_clauses(`
`47`	`47`	`if result.is_empty() {`
`48`	`48`	`None`
`49`	`49`	`} else {`
`50`		`- Some(ConflictClause::combine(result.as_slice()))`
	`50`	`+ let c = ConflictClause::combine(result.as_slice());`
	`51`	`+ if c.decisions().is_empty() {`
	`52`	`+ None`
	`53`	`+ } else {`
	`54`	`+ Some(c)`
	`55`	`+ }`
`51`	`56`	`}`
`52`	`57`	`}`