Added the ability to reason about conditionals without else branches.
Allowing conditional guards to be expressed using = and != predicates.
Picus findings are now visible on the findings table.
Picus now emits informational findings when the analysis contains unknown results.
Support for conditionals in the Picus Constraint Language and updated the verification logic and range analysis to handle conditionals in a limited fashion for now.
Support for specifying and verifying postconditions for modules. Currently those postconditions are not used in the parent modules.
Conditionals of the form (if poly (A) (B)) have the semantics poly != 0 => A /\ poly = 0 => B. This is the more natural semantics in ZK circuits since these statements are lowered to constraints by multiplying the constraints by poly in the then branch.
Add a multi-solver option which runs both cvc5-int and cvc5-ff on every SMT query.
Add a new optional parameter –apply-rewrites which, when enabled, causes Picus to rewrite constraints into a form more friendly for its uniqueness propagators. Currently disabled by default as it is not robustly tested.
Added a new construct assume-deterministic to the picus language which allows user to directly specify whether a signal is deterministic even if it isn't an input to the circuit. This is useful for AIR based circuits which reference signals in previous columns.
More error checking on inputs. We now validate that the call graph is not recursive and that all calls to submodules point to actual subcircuits.