Allow `java_symexec` to return safety condition
Allow `java_symexec` to return safety condition

The special variable named "$safety", when included in the outputs list
for `java_symexec`, corresponds to the safety condition of the symbolic
execution run. If you can prove that it's valid, the other terms
returned should be semantically correct.

GaloisInc/saw-script,GaloisInc/saw-script,GaloisInc/saw-script,GaloisInc/saw-script,GaloisInc/saw-script