When Z3 is available, macro test cases are failing. The problem is that we cannot use conditional directives because FileCheck is not preprocessing the source file before doing the comparison. So before
doing the verification we are preprocessing the test file.
Another thing is that the preprocessing command doesn't know that Z3 is turned on or not so we are using variable substitution to tell it.
When
Z3
is available, macro test cases are failing. The problem is that we cannot use conditional directives becauseFileCheck
is not preprocessing the source file before doing the comparison. So before doing the verification we are preprocessing the test file.Another thing is that the preprocessing command doesn't know that Z3 is turned on or not so we are using variable substitution to tell it.