Skip to content

Commit

Permalink
[regression] adjusted windows TC
Browse files Browse the repository at this point in the history
  • Loading branch information
XLiZHI authored and lucasccordeiro committed Apr 15, 2024
1 parent 97b8193 commit dc97df8
Show file tree
Hide file tree
Showing 3 changed files with 29 additions and 1 deletion.
@@ -1,4 +1,4 @@
CORE
THOROUGH
main.cpp
--k-induction
^VERIFICATION FAILED$
24 changes: 24 additions & 0 deletions regression/windows/cpp_priority_queue_size_bug/main.cpp
@@ -0,0 +1,24 @@
// priority_queue::size
#include <cassert>
#include <cstdlib>
#include <queue>

using namespace std;

int nondet_int();
int N = nondet_int();

int main ()
{
__ESBMC_assume(N>0);

priority_queue<int> myints;

for (int i=0; i<=N; i++)
myints.push(i);

assert(myints.size() == N+1);
myints.pop();
assert(myints.size() == N+1);
return 0;
}
4 changes: 4 additions & 0 deletions regression/windows/cpp_priority_queue_size_bug/test.desc
@@ -0,0 +1,4 @@
KNOWNBUG
main.cpp
--k-induction
^VERIFICATION FAILED$

0 comments on commit dc97df8

Please sign in to comment.