diff --git a/CMakeLists.txt b/CMakeLists.txt index 8b8a71e..7ccd40c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -18,6 +18,8 @@ cmake_minimum_required(VERSION 2.8) enable_language(C) enable_language(CXX) +set(CMAKE_POSITION_INDEPENDENT_CODE ON) + if(NOT CMAKE_BUILD_TYPE) set(CMAKE_BUILD_TYPE Release) endif() diff --git a/examples/Primes.cpp b/examples/Primes.cpp index f99c9bc..161527d 100644 --- a/examples/Primes.cpp +++ b/examples/Primes.cpp @@ -41,6 +41,19 @@ TEST(PrimePolynomial, OnlyGeneratesPrimes) { << x << "^2 + " << x << " + 41 is not prime"; } +TEST(PrimePolynomial, OnlyGeneratesPrimes_NoStreaming) { + symbolic_unsigned x, y, z; + DeepState_Assume(x > 0); + unsigned poly = (x * x) + x + 41; + DeepState_Assume(y > 1); + DeepState_Assume(z > 1); + DeepState_Assume(y < poly); + DeepState_Assume(z < poly); + DeepState_Assert(poly != (y * z)); + DeepState_Assert(IsPrime(Pump(poly))); +} + + int main(int argc, char *argv[]) { DeepState_InitOptions(argc, argv); return DeepState_Run();