Z3 timeout

[anothermattbrown]

Added a batfish setting for Z3's timeout parameter. Passed it to Z3 in Minesweeper's PropertyChecker and Batfish's NodJob and CompositNodJob classes. Had to add some plumbing to get the Settings object to PropertyChecker.

---

This change is 

[dhalperi]

High-level LGTM.

Most of the code gets the settings by calling Main.getSettings() or something like that, but I actually prefer injecting it as your SMT changes are structured. Static shared state prevents us from running more than 1 worker in the same process, makes testing harder, etc.

---

Reviewed 10 of 10 files at r1.
Review status: all files reviewed at latest revision, 2 unresolved discussions.

---

tests/basic/z3timeout.ref, line 11 at r1 (raw file):

        "   at org.batfish.main.Driver$1.run(Driver.java:367)",
        "Caused by: org.batfish.common.BatfishException: Error executing job",
        "   at org.batfish.job.BatfishJobExecutor.executeJobs(BatfishJobExecutor.java:129)",

This test is brittle -- it's going to require updating the ref anytime code changes (Batfish.java line numbers, for example).

I think there's a different test that simply expects an error, try to find that one?

---

tests/java-smt/commands, line 143 at r1 (raw file):

# z3 timeout - 1 second
add-batfish-option z3timeout 1000

why not 1ms?

---

Comments from Reviewable

[anothermattbrown]

Review status: all files reviewed at latest revision, 2 unresolved discussions.

---

tests/basic/z3timeout.ref, line 11 at r1 (raw file):

Previously, dhalperi (Dan Halperin) wrote…

This test is brittle -- it's going to require updating the ref anytime code changes (Batfish.java line numbers, for example).

I think there's a different test that simply expects an error, try to find that one?

Aha, looks like the ref file isn't checked for -error tests, so I could use an empty ref file instead.
The only other -error test is tests/basic/error.ref, which also could be made less brittle by emptying the file.

---

tests/java-smt/commands, line 143 at r1 (raw file):

Previously, dhalperi (Dan Halperin) wrote…

why not 1ms?

good idea

---

Comments from Reviewable

[dhalperi]

Reviewed 4 of 4 files at r2.
Review status: all files reviewed at latest revision, all discussions resolved.

---

Comments from Reviewable

[dhalperi]

---

Comments from Reviewable