1 #include <gtest/gtest.h>
2 #include <stdio.h>
3 #include <stp/c_interface.h>
4
TEST(counter_example_reading,one)5 TEST(counter_example_reading, one)
6 {
7
8 VC vc = vc_createValidityChecker();
9 Expr falseExpr = vc_falseExpr(vc);
10
11 Expr A = vc_varExpr(vc, "A", vc_bv32Type(vc));
12 Expr B = vc_varExpr(vc, "B", vc_bv32Type(vc));
13
14 vc_push(vc);
15
16 Expr AplusB = vc_bv32PlusExpr(vc, A, B);
17 Expr AplusBplus42 =
18 vc_bv32PlusExpr(vc, AplusB, vc_bv32ConstExprFromInt(vc, 42));
19
20 assert(0 == vc_query(vc, falseExpr));
21
22 // Don't do this,
23 #if 0
24 WholeCounterExample wce = vc_getWholeCounterExample(vc);
25 uint32_t a = getBVUnsigned(vc_getTermFromCounterExample(vc, A, wce));
26 uint32_t b = getBVUnsigned(vc_getTermFromCounterExample(vc, B, wce));
27 uint32_t sum = getBVUnsigned(vc_getTermFromCounterExample(vc, AplusBplus42, wce));
28 vc_deleteWholeCounterExample(wce);
29 #endif
30
31 // Do this instead.
32 vc_getCounterExample(vc, A);
33 uint32_t a = getBVUnsigned(vc_getCounterExample(vc, A));
34 uint32_t b = getBVUnsigned(vc_getCounterExample(vc, B));
35 uint32_t sum = getBVUnsigned(vc_getCounterExample(vc, AplusBplus42));
36
37 ASSERT_TRUE(sum == a + b + 42);
38
39 vc_Destroy(vc);
40 }
41