Hoang M. Le

I was about to raise a similar issue before finding this. Such check would definitely have prevented #1034 :) I'd push for actually building an executable and run it with...

The Test-Comp validator and some testers actually link in the nondet functions and run the benchmarks. In an isolated environment (and with sanitizers enabled) I guess it is acceptable, but...

Given that most PRs only touch a (small) subset of tasks, I think the most impactful and (simple) optimization is to avoid checking unchanged tasks. Isn't it already enough to...

Yes, that should be implemented as a top-level heuristic. If a PR changes *.i and *.c only (most PRs do), then you are safe, otherwise just run a full CI...

I guess `if $TRAVIS_PULL_REQUEST then git diff $TRAVIS_BRANCH --name-only` would do the job, to also support push builds, we would need `$TRAVIS_COMMIT_RANGE` (these enviroment variables are defined here https://docs.travis-ci.com/user/environment-variables/#convenience-variables)

@ccadar thanks for the reminder, I'll try to finish the PR next week

That is unexpected, the sudoku examples should finish under 20s with CUDD and much faster with Boolector. Which CRAVE version are you using and your environment specs?

@chiragv44 as @finnhaedicke has correctly explained, CRAVE does not forbid overflow, so the results you got are technically correct. If you do not want this behavior, the easiest workaround is...

We did not intend to support manipulation of the randv/rand_obj object tree from user code, but it would have been useful to detach objects on their destruction to prevent such...

We should definitely follow the standard here and fix this as it is (still) easy to fix. Thanks!