================
@@ -74,13 +74,13 @@ TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) {
}
TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
}
----------------
steakhal wrote:
I don't think these test reflect what they were testing anymore. Similar
argument goes for the rest of the test cases.
The test name suggests `UNSATWhenItGoesOverTime`, so we should pass a time that
meets this scenario with the new timeout of 15 seconds. I suppose `15'010_ms`
should suffice.
It would be also nice if we could showcase the difference of the non-default
(previous) config with using 400k rlimit and 300ms timeout to see if the
behavior still meets the expected behavior of we had.
It shouldn't be much of a burden to create that config - similar how the
`DefaultOpts` is made, and basically copy-paste the original tests. We could
have a separate fixture for it, called `Z3CrosscheckDefaultOracleTest` and a
`Z3CrosscheckCustomOracleTest` where the defaults are overridden. This way even
the PR diff would look nice.
https://github.com/llvm/llvm-project/pull/118291
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
