Cristian Cadar

Just curious, is there a new release being planned? The last one is really old now.

Thanks @rgov. Indeed, ideally across OSes, but even on the same machine it's useful. Essentially, we observed that both the counterexamples returned by STP and its execution time vary across...

Thanks, @msoos . For reference, the patch removing these options is d804c9753971e. Most likely there are other sources of non-determinism, but we'll try the latest version and let you know.

Hi @msoos , just to make sure that we are on the same page with @MartinNowack 's example. We are talking about: (1) The same query given in one file...

Thanks, @zvonimir . I don't see this in the Test-Comp rules. Just curious, where is this mentioned in the SV-COMP rules? I grepped for "library" and "standard" in https://sv-comp.sosy-lab.org/2019/rules.php but...

:) I think it would be really useful to spell these things out, to make it easier for others to get involved. Perhaps such discussions are a good time to...

@MartinSpiessl I think adding the text you propose is useful and important.

@lembergerth , @dbeyer has anyone looked at this? I think this benchmark needs to be removed from Test-Comp.

Hi @shaobo-he, sorry for the delayed response. The issue here is that we use Z3's parser via its public API, which only seems to allow us to extract the constraints...

Do you mean solving constraints in the theory of strings? If so, you need to map the string operations into C equivalents, e.g., `indexOf` into `strchr`. Does this answer your...