Skip to content

Commit e09c73e

Browse files
committed
Prevent reduction of Std.Sat.AIG.denote
1 parent e72eadd commit e09c73e

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Std/Sat/AIG/Basic.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -485,6 +485,7 @@ where
485485
let lval := go lhs.gate decls assign (by omega) h2
486486
let rval := go rhs.gate decls assign (by omega) h2
487487
xor lval lhs.invert && xor rval rhs.invert
488+
termination_by (x, 0) -- Don't allow reduction, we have large concrete gate entries
488489

489490
/--
490491
Denotation of an `AIG` at a specific `Entrypoint`.

0 commit comments

Comments
 (0)