DeforaNetworks/deepstate
3
0
Fork 0
Code Releases Activity

Enabled PIC.

Browse Source
This commit is contained in:
Peter Goodman
2018-01-22 21:19:54 -05:00
parent ee80baa0ea
commit d227cc7f34
2 changed files with 15 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
examples/Primes.cpp
+13
View File
@@ -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();