Fix assertion failure in Abc_AigUpdateLevelR_int during refactor/rewrite/resub

[jfkey]

Description

This PR fixes a long-standing assertion failure that occurs during logic synthesis commands such as refactor, rewrite, and resub. The crash happens when updating the reverse level of nodes.

Fixes Issues:
issue #271
issue #451
issue #457

Error Log

When running specific benchmarks, the tool aborts with the following assertion error:

abc: src/base/abc/abcAig.c:1134: Abc_AigUpdateLevelR_int: Assertion `Abc_ObjIsNode(pNode)' failed.
Aborted (core dumped)

Root Cause

The issue is located in the Abc_AigUpdateLevelR_int function. During the recursive update of reverse levels for fanin nodes, the function attempts to process all reachable nodes. However, it failed to filter out constant nodes.

When the traversal encounters a constant node, the assertion Abc_ObjIsNode(pNode) fails because a constant is not considered a standard logic node in this context. The fix ensures that constant nodes are skipped during the reverse level update.

Reproduction Steps

The crash can be reproduced using the test cases provided in the related issues (files available here).

Case 1:

./abc -c "read int2float-24.aig; refactor"

Case 2:

./abc -c "read RISC.aig; rewrite"

Case 3:

./abc -c "read crash_retcode_case.blif; rewrite"

Solution

Modified the traversal logic in Abc_AigUpdateLevelR_int to explicitly check for and skip constant nodes before attempting to access/update their reverse levels.