Commit 43a86ca
committed
Fix book regression tests handling of smt test runs
The `CMakeLists.txt` for the `book-examples` directory appears to be
based on a copy of the one from the `regression/cbmc` directory.
Unfortunately the first parameter to `add_test_pl_profile` needs to be
unique and it has not been updated to a unique name for the new file.
This was resulting in the existing tests not being run.1 parent cf380d5 commit 43a86ca
1 file changed
+3
-3
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
24 | 24 | | |
25 | 25 | | |
26 | 26 | | |
27 | | - | |
| 27 | + | |
28 | 28 | | |
29 | 29 | | |
30 | 30 | | |
31 | 31 | | |
32 | 32 | | |
33 | 33 | | |
34 | 34 | | |
35 | | - | |
| 35 | + | |
36 | 36 | | |
37 | 37 | | |
38 | 38 | | |
| |||
41 | 41 | | |
42 | 42 | | |
43 | 43 | | |
44 | | - | |
| 44 | + | |
45 | 45 | | |
46 | 46 | | |
47 | 47 | | |
| |||
0 commit comments