This directory contains experiments using primarily 3rd-party code, eg. bounded-model-checking with ReluPlex and precondition-computation with ERAN. They are packaged as Docker containers which can be run using Bazel scripts from the base of this repository.