SMT can and will timeout on some traces, we can't do anything with it. However it's important to do timeouts per trace, not per whole file. Now we can set time limit per file with MULTIPLE traces (by passing -T 5 as command line argument to Z3), so when first of them timeout we will abort the following traces. We can embed timeout into formula itself making it per trace.
SMT can and will timeout on some traces, we can't do anything with it. However it's important to do timeouts per trace, not per whole file. Now we can set time limit per file with MULTIPLE traces (by passing
-T 5as command line argument to Z3), so when first of them timeout we will abort the following traces. We can embed timeout into formula itself making it per trace.