Skip to content

Commit

Permalink
Fix for let def PO
Browse files Browse the repository at this point in the history
  • Loading branch information
@nickbattle
nickbattle committed Sep 11, 2023
1 parent a6b1a28 commit 5cd1063
Show file tree
Hide file tree
Showing 3 changed files with 89 additions and 89 deletions.
2 changes: 1 addition & 1 deletion vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POLetDefExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@ public String toString()
@Override
public ProofObligationList getProofObligations(POContextStack ctxt, Environment env)
{
ctxt.push(new POLetDefContext(this.localDefs)); // See bug #6
ProofObligationList obligations = localDefs.getDefProofObligations(ctxt, env);
ctxt.push(new POLetDefContext(this.localDefs)); // See bug #6
obligations.addAll(expression.getProofObligations(ctxt, env));
ctxt.pop();

Expand Down
2 changes: 1 addition & 1 deletion vdmj/src/main/java/com/fujitsu/vdmj/pog/POStatus.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@

public enum POStatus
{
UNPROVED("Unproved"), PROVED("Proved"), TRIVIAL("Trivial"), UNCHECKED("Unchecked");
UNPROVED("Unproved"), PROVED("Proved"), TRIVIAL("Trivial"), MAYBE("Maybe"), UNCHECKED("Unchecked");

private String text;

Expand Down
174 changes: 87 additions & 87 deletions vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,92 +65,92 @@ protected void tearDown() throws Exception

private String[] expected =
{
"(forall a:seq of (nat1) &\n is_(inv_T2(a), bool))\n",
"exists a : seq of (nat1) & (a <> [])\n",
"forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
"After instance variable initializers (iv < 10)\n",
"forall arg1:(int * int), arg2:seq of (int) & (exists bind1:(int * int), i:int, j:int & (arg1 = bind1) and (mk_(i, j) = bind1)) and (exists bind1:seq of (int), k:int & (arg2 = bind1) and ([k] = bind1))\n",
"(forall mk_(i, j):(int * int), [k]:seq of (int) &\n i in set dom m)\n",
"(forall mk_(i, j):(int * int) &\n i in set dom m)\n",
"(let x:nat1 = 123 in\n -1 in set dom m)\n",
"(let x:nat1 = 123 in\n ((m(-1) > 0) =>\n 1 in set dom m))\n",
"(let x:nat1 = 123 in\n (not (m(-1) > 0) =>\n -2 in set dom m))\n",
"(let x:nat1 = 123 in\n (not (m(-1) > 0) =>\n ((m(-2) > 0) =>\n 2 in set dom m)))\n",
"(let x:nat1 = 123 in\n (not (m(-1) > 0) =>\n (not (m(-2) > 0) =>\n (((x < 0) or ((x > 10) or (x = 100))) =>\n 3 in set dom m))))\n",
"(let x:nat1 = 123 in\n (not (m(-1) > 0) =>\n (not (m(-2) > 0) =>\n (not ((x < 0) or ((x > 10) or (x = 100))) =>\n 999 in set dom m))))\n",
"(forall a:int, b:int & pre_pref(a, b) =>\n a in set dom m)\n",
"(forall a:int, b:int &\n pre_prepostf(a, b) => post_prepostf(a, b, (a + b)))\n",
"(forall mk_(a, b):(int * int), c:(int * int) &\n is_(pre_prepostfi(mk_(a, b), c), bool))\n",
"(forall mk_(a, b):(int * int), c:(int * int) &\n pre_prepostfi(mk_(a, b), c) => exists r:int & post_prepostfi(mk_(a, b), c, r))\n",
"(forall x:seq of (int) &\n (exists [a]:seq1 of (int) & [a] = (x ^ [-999]) => let [a] = (x ^ [-999]) in\n a in set dom m))\n",
"(forall x:seq of (int) &\n (not exists [a]:seq1 of (int) & [a] = (x ^ [-999]) =>\n (exists [a, b]:seq1 of (int) & [a, b] = (x ^ [-999]) => let [a, b] = (x ^ [-999]) in\n (a + b) in set dom m)))\n",
"(forall x:seq of (int) &\n (not exists [a]:seq1 of (int) & [a] = (x ^ [-999]) =>\n (not exists [a, b]:seq1 of (int) & [a, b] = (x ^ [-999]) =>\n (exists [a] ^ [b]:seq1 of (int) & ([a] ^ [b]) = (x ^ [-999]) => let [a] ^ [b] = (x ^ [-999]) in\n (a + b) in set dom m))))\n",
"(forall x:seq of (int) &\n (not exists [a]:seq1 of (int) & [a] = (x ^ [-999]) =>\n (not exists [a, b]:seq1 of (int) & [a, b] = (x ^ [-999]) =>\n (not exists [a] ^ [b]:seq1 of (int) & ([a] ^ [b]) = (x ^ [-999]) =>\n m(999) in set dom m))))\n",
"(forall x:seq of (int) &\n (not exists [a]:seq1 of (int) & [a] = (x ^ [-999]) =>\n (not exists [a, b]:seq1 of (int) & [a, b] = (x ^ [-999]) =>\n (not exists [a] ^ [b]:seq1 of (int) & ([a] ^ [b]) = (x ^ [-999]) =>\n 999 in set dom m))))\n",
"(forall mk_(i, $any1):(int * int) &\n exists x in set {m(1), 2, 3} & (m(x) < i))\n",
"(forall mk_(i, $any1):(int * int) &\n 1 in set dom m)\n",
"(forall mk_(i, $any1):(int * int) &\n (forall x in set {m(1), 2, 3} &\n x in set dom m))\n",
"(forall mk_(i, $any1):(int * int) &\n (forall x in set {m(1), 2, 3} & (m(x) < i) =>\n x in set dom m))\n",
"(let x:int = m(1) in\n 1 in set dom m)\n",
"(let x:int = m(1) in\n x in set dom m)\n",
"(let local: int -> int local(x) == m(x) in\n (forall x:int &\n x in set dom m))\n",
"1 in set dom m\n",
"(let x = m(1) in\n 2 in set dom m)\n",
"(def x = m(1); y = m(2) in\n x in set dom m)\n",
"(def x = m(1); y = m(2) in\n y in set dom m)\n",
"exists1 x in set {1, 2, 3} & (x < 10)\n",
"(forall n:nat &\n n > 1 => forall arg:nat & pre_f1(arg) => pre_f1(f1(arg)))\n",
"(forall x:(int -> int), n:nat &\n n > 1 => forall arg:nat & pre_(x, arg) => pre_(x, x(arg)))\n",
"(forall n:nat &\n n = 0 or n = 1 or rng(m) subset dom(m))\n",
"(forall x:map (int) to (int), n:nat &\n n = 0 or n = 1 or rng(x) subset dom(x))\n",
"forall arg:int & pre_f2(arg) => pre_f1(f2(arg))\n",
"(forall x:(int -> int), y:(int -> int) &\n forall arg:int & pre_(y, arg) => pre_(x, y(arg)))\n",
"(forall x:(int -> int) &\n forall arg:int & pre_f2(arg) => pre_(x, f2(arg)))\n",
"(forall x:(int -> int) &\n forall arg:int & pre_(x, arg) => pre_f1(x(arg)))\n",
"rng(m) subset dom(m)\n",
"(forall x:map (int) to (int), y:map (int) to (int) &\n rng(y) subset dom(x))\n",
"(forall x:map (int) to (int) &\n rng(m) subset dom(x))\n",
"(forall i:int &\n pre_f1(i))\n",
"(forall x:(int -> int) &\n pre_(x, 123))\n",
"(forall i:int &\n i in set inds sq)\n",
"(forall x:seq of (int) &\n 123 in set inds x)\n",
"(forall s:set of (set of (int)) &\n s <> {})\n",
"(forall s:seq of (int) &\n (not (s = []) =>\n s <> []))\n",
"(forall i:int &\n i <> 0)\n",
"(forall i:int &\n is_int((123 / i)))\n",
"(forall i:int &\n i <> 0)\n",
"exists finmap1:map nat to (map (int) to (nat1)) & forall a:int, b in set {1, 2, 3} & (a < 10) => exists findex2 in set dom finmap1 & finmap1(findex2) = {a |-> b}\n",
"exists finmap1:map nat to (int) & forall a:int, b in set {1, 2, 3} & (a < 10) => exists findex2 in set dom finmap1 & finmap1(findex2) = (a + b)\n",
"(forall a:map (int) to (int), b:map (int) to (int) &\n forall ldom1 in set dom a, rdom2 in set dom b & ldom1 = rdom2 => a(ldom1) = b(rdom2))\n",
"(forall x:int &\n forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}, {x |-> 4}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4))\n",
"forall m1 in set {{1 |-> 2}, {2 |-> 3}}, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
"(forall n:nat &\n is_(measure_recursive(n), nat))\n",
"(forall n:nat &\n (not (n = 1) =>\n (n - 1) >= 0))\n",
"(forall n:nat &\n (not (n = 1) =>\n measure_recursive(n) > measure_recursive((n - 1))))\n",
"dom {1 |-> false} subset inds [2, true, 7.8]\n",
"is_(([2, true, 7.8] ++ {1 |-> false}), seq of ((bool | nat)))\n",
"(forall t:((nat * nat * nat) | (nat * nat)) &\n is_(t, (nat * nat * nat)))\n",
"(forall u:U &\n (let mk_(a, b):U = u in\n exists mk_(a, b):U & mk_(a, b) = u))\n",
"(forall u:U &\n (let mk_(a, b):U = u in\n is_(u, (nat * nat))))\n",
"(is_([1, 2, true], T1) and ((is_(1, bool)) and (is_(2, bool)))) or (is_([1, 2, true], T2) and inv_T2([1, 2, true]) and ((is_nat1(true))))\n",
"(forall t:(T1 | T2) &\n (let x:(T1 | T2) = [1, 2, 3, true] in\n (is_([1, 2, 3, true], T1) and ((is_(1, bool)) and (is_(2, bool)) and (is_(3, bool)))) or (is_([1, 2, 3, true], T2) and inv_T2([1, 2, 3, true]) and ((is_nat1(true))))))\n",
"(forall a:(T1 | T2 | int) &\n (is_(a, T1)) or (is_(a, T2) and inv_T2(a) and (is_(a, seq of (nat1)))))\n",
"is_({1 |-> \"2\"}, inmap nat1 to seq1 of (char))\n",
"(forall n:nat1, x:nat1 &\n (not (n < 2) =>\n (n - 1) > 0))\n",
"(forall n:nat1, x:nat1 &\n (not (n < 2) =>\n (x - 1) > 0))\n",
"(forall n:nat1, x:nat1 &\n (not (n < 2) =>\n id(n, x) > id((n - 1), (x - 1))))\n",
"(forall x:nat1, y:nat1 &\n (x - y) >= 0)\n",
"(forall mk_(n, x):(nat1 * nat1) &\n (not (n < 2) =>\n ((n - 1) > 0) and ((x - 1) > 0)))\n",
"(forall mk_(n, x):(nat1 * nat1) &\n (not (n < 2) =>\n id2(mk_(n, x)) > id2(mk_((n - 1), (x - 1)))))\n",
"(forall mk_(x, y):(nat1 * nat1) &\n (x - y) >= 0)\n",
"(forall mk_(n, x):(nat1 * nat1) &\n (not (n < 2) =>\n ((n - 1) > 0) and ((x - 1) > 0)))\n",
"(forall mk_(n, x):(nat1 * nat1) &\n (not (n < 2) =>\n (let lhs = id3(mk_(n, x)), rhs = id3(mk_((n - 1), (x - 1))) in if lhs.#1 <> rhs.#1 then lhs.#1 > rhs.#1 else lhs.#2 > rhs.#2)))\n",
"1 in set dom m\n",
"1 in set dom m\n",
"2 in set dom m\n",
"3 in set dom m\n",
"while (x > 0) do ...\n",
"After iv := (iv + 1) (iv < 10)\n"
/* 1 */ "(forall a:seq of (nat1) &\n is_(inv_T2(a), bool))\n",
/* 2 */ "exists a : seq of (nat1) & (a <> [])\n",
/* 3 */ "forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
/* 4 */ "After instance variable initializers (iv < 10)\n",
/* 5 */ "forall arg1:(int * int), arg2:seq of (int) & (exists bind1:(int * int), i:int, j:int & (arg1 = bind1) and (mk_(i, j) = bind1)) and (exists bind1:seq of (int), k:int & (arg2 = bind1) and ([k] = bind1))\n",
/* 6 */ "(forall mk_(i, j):(int * int), [k]:seq of (int) &\n i in set dom m)\n",
/* 7 */ "(forall mk_(i, j):(int * int) &\n i in set dom m)\n",
/* 8 */ "(let x:nat1 = 123 in\n -1 in set dom m)\n",
/* 9 */ "(let x:nat1 = 123 in\n ((m(-1) > 0) =>\n 1 in set dom m))\n",
/* 10 */ "(let x:nat1 = 123 in\n (not (m(-1) > 0) =>\n -2 in set dom m))\n",
/* 11 */ "(let x:nat1 = 123 in\n (not (m(-1) > 0) =>\n ((m(-2) > 0) =>\n 2 in set dom m)))\n",
/* 12 */ "(let x:nat1 = 123 in\n (not (m(-1) > 0) =>\n (not (m(-2) > 0) =>\n (((x < 0) or ((x > 10) or (x = 100))) =>\n 3 in set dom m))))\n",
/* 13 */ "(let x:nat1 = 123 in\n (not (m(-1) > 0) =>\n (not (m(-2) > 0) =>\n (not ((x < 0) or ((x > 10) or (x = 100))) =>\n 999 in set dom m))))\n",
/* 14 */ "(forall a:int, b:int & pre_pref(a, b) =>\n a in set dom m)\n",
/* 15 */ "(forall a:int, b:int &\n pre_prepostf(a, b) => post_prepostf(a, b, (a + b)))\n",
/* 16 */ "(forall mk_(a, b):(int * int), c:(int * int) &\n is_(pre_prepostfi(mk_(a, b), c), bool))\n",
/* 17 */ "(forall mk_(a, b):(int * int), c:(int * int) &\n pre_prepostfi(mk_(a, b), c) => exists r:int & post_prepostfi(mk_(a, b), c, r))\n",
/* 18 */ "(forall x:seq of (int) &\n (exists [a]:seq1 of (int) & [a] = (x ^ [-999]) => let [a] = (x ^ [-999]) in\n a in set dom m))\n",
/* 19 */ "(forall x:seq of (int) &\n (not exists [a]:seq1 of (int) & [a] = (x ^ [-999]) =>\n (exists [a, b]:seq1 of (int) & [a, b] = (x ^ [-999]) => let [a, b] = (x ^ [-999]) in\n (a + b) in set dom m)))\n",
/* 20 */ "(forall x:seq of (int) &\n (not exists [a]:seq1 of (int) & [a] = (x ^ [-999]) =>\n (not exists [a, b]:seq1 of (int) & [a, b] = (x ^ [-999]) =>\n (exists [a] ^ [b]:seq1 of (int) & ([a] ^ [b]) = (x ^ [-999]) => let [a] ^ [b] = (x ^ [-999]) in\n (a + b) in set dom m))))\n",
/* 21 */ "(forall x:seq of (int) &\n (not exists [a]:seq1 of (int) & [a] = (x ^ [-999]) =>\n (not exists [a, b]:seq1 of (int) & [a, b] = (x ^ [-999]) =>\n (not exists [a] ^ [b]:seq1 of (int) & ([a] ^ [b]) = (x ^ [-999]) =>\n m(999) in set dom m))))\n",
/* 22 */ "(forall x:seq of (int) &\n (not exists [a]:seq1 of (int) & [a] = (x ^ [-999]) =>\n (not exists [a, b]:seq1 of (int) & [a, b] = (x ^ [-999]) =>\n (not exists [a] ^ [b]:seq1 of (int) & ([a] ^ [b]) = (x ^ [-999]) =>\n 999 in set dom m))))\n",
/* 23 */ "(forall mk_(i, $any1):(int * int) &\n exists x in set {m(1), 2, 3} & (m(x) < i))\n",
/* 24 */ "(forall mk_(i, $any1):(int * int) &\n 1 in set dom m)\n",
/* 25 */ "(forall mk_(i, $any1):(int * int) &\n (forall x in set {m(1), 2, 3} &\n x in set dom m))\n",
/* 26 */ "(forall mk_(i, $any1):(int * int) &\n (forall x in set {m(1), 2, 3} & (m(x) < i) =>\n x in set dom m))\n",
/* 27 */ "1 in set dom m\n",
/* 28 */ "(let x:int = m(1) in\n x in set dom m)\n",
/* 29 */ "(forall x:int &\n x in set dom m)\n",
/* 30 */ "1 in set dom m\n",
/* 31 */ "(let x = m(1) in\n 2 in set dom m)\n",
/* 32 */ "(def x = m(1); y = m(2) in\n x in set dom m)\n",
/* 33 */ "(def x = m(1); y = m(2) in\n y in set dom m)\n",
/* 34 */ "exists1 x in set {1, 2, 3} & (x < 10)\n",
/* 35 */ "(forall n:nat &\n n > 1 => forall arg:nat & pre_f1(arg) => pre_f1(f1(arg)))\n",
/* 36 */ "(forall x:(int -> int), n:nat &\n n > 1 => forall arg:nat & pre_(x, arg) => pre_(x, x(arg)))\n",
/* 37 */ "(forall n:nat &\n n = 0 or n = 1 or rng(m) subset dom(m))\n",
/* 38 */ "(forall x:map (int) to (int), n:nat &\n n = 0 or n = 1 or rng(x) subset dom(x))\n",
/* 39 */ "forall arg:int & pre_f2(arg) => pre_f1(f2(arg))\n",
/* 40 */ "(forall x:(int -> int), y:(int -> int) &\n forall arg:int & pre_(y, arg) => pre_(x, y(arg)))\n",
/* 41 */ "(forall x:(int -> int) &\n forall arg:int & pre_f2(arg) => pre_(x, f2(arg)))\n",
/* 42 */ "(forall x:(int -> int) &\n forall arg:int & pre_(x, arg) => pre_f1(x(arg)))\n",
/* 43 */ "rng(m) subset dom(m)\n",
/* 44 */ "(forall x:map (int) to (int), y:map (int) to (int) &\n rng(y) subset dom(x))\n",
/* 45 */ "(forall x:map (int) to (int) &\n rng(m) subset dom(x))\n",
/* 46 */ "(forall i:int &\n pre_f1(i))\n",
/* 47 */ "(forall x:(int -> int) &\n pre_(x, 123))\n",
/* 48 */ "(forall i:int &\n i in set inds sq)\n",
/* 49 */ "(forall x:seq of (int) &\n 123 in set inds x)\n",
/* 50 */ "(forall s:set of (set of (int)) &\n s <> {})\n",
/* 51 */ "(forall s:seq of (int) &\n (not (s = []) =>\n s <> []))\n",
/* 52 */ "(forall i:int &\n i <> 0)\n",
/* 53 */ "(forall i:int &\n is_int((123 / i)))\n",
/* 54 */ "(forall i:int &\n i <> 0)\n",
/* 55 */ "exists finmap1:map nat to (map (int) to (nat1)) & forall a:int, b in set {1, 2, 3} & (a < 10) => exists findex2 in set dom finmap1 & finmap1(findex2) = {a |-> b}\n",
/* 56 */ "exists finmap1:map nat to (int) & forall a:int, b in set {1, 2, 3} & (a < 10) => exists findex2 in set dom finmap1 & finmap1(findex2) = (a + b)\n",
/* 57 */ "(forall a:map (int) to (int), b:map (int) to (int) &\n forall ldom1 in set dom a, rdom2 in set dom b & ldom1 = rdom2 => a(ldom1) = b(rdom2))\n",
/* 58 */ "(forall x:int &\n forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}, {x |-> 4}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4))\n",
/* 59 */ "forall m1 in set {{1 |-> 2}, {2 |-> 3}}, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
/* 60 */ "(forall n:nat &\n is_(measure_recursive(n), nat))\n",
/* 61 */ "(forall n:nat &\n (not (n = 1) =>\n (n - 1) >= 0))\n",
/* 62 */ "(forall n:nat &\n (not (n = 1) =>\n measure_recursive(n) > measure_recursive((n - 1))))\n",
/* 63 */ "dom {1 |-> false} subset inds [2, true, 7.8]\n",
/* 64 */ "is_(([2, true, 7.8] ++ {1 |-> false}), seq of ((bool | nat)))\n",
/* 65 */ "(forall t:((nat * nat * nat) | (nat * nat)) &\n is_(t, (nat * nat * nat)))\n",
/* 66 */ "(forall u:U &\n exists mk_(a, b):U & mk_(a, b) = u)\n",
/* 67 */ "(forall u:U &\n is_(u, (nat * nat)))\n",
/* 68 */ "(is_([1, 2, true], T1) and ((is_(1, bool)) and (is_(2, bool)))) or (is_([1, 2, true], T2) and inv_T2([1, 2, true]) and ((is_nat1(true))))\n",
/* 69 */ "(forall t:(T1 | T2) &\n (is_([1, 2, 3, true], T1) and ((is_(1, bool)) and (is_(2, bool)) and (is_(3, bool)))) or (is_([1, 2, 3, true], T2) and inv_T2([1, 2, 3, true]) and ((is_nat1(true)))))\n",
/* 70 */ "(forall a:(T1 | T2 | int) &\n (is_(a, T1)) or (is_(a, T2) and inv_T2(a) and (is_(a, seq of (nat1)))))\n",
/* 71 */ "is_({1 |-> \"2\"}, inmap nat1 to seq1 of (char))\n",
/* 72 */ "(forall n:nat1, x:nat1 &\n (not (n < 2) =>\n (n - 1) > 0))\n",
/* 73 */ "(forall n:nat1, x:nat1 &\n (not (n < 2) =>\n (x - 1) > 0))\n",
/* 74 */ "(forall n:nat1, x:nat1 &\n (not (n < 2) =>\n id(n, x) > id((n - 1), (x - 1))))\n",
/* 75 */ "(forall x:nat1, y:nat1 &\n (x - y) >= 0)\n",
/* 76 */ "(forall mk_(n, x):(nat1 * nat1) &\n (not (n < 2) =>\n ((n - 1) > 0) and ((x - 1) > 0)))\n",
/* 77 */ "(forall mk_(n, x):(nat1 * nat1) &\n (not (n < 2) =>\n id2(mk_(n, x)) > id2(mk_((n - 1), (x - 1)))))\n",
/* 78 */ "(forall mk_(x, y):(nat1 * nat1) &\n (x - y) >= 0)\n",
/* 79 */ "(forall mk_(n, x):(nat1 * nat1) &\n (not (n < 2) =>\n ((n - 1) > 0) and ((x - 1) > 0)))\n",
/* 80 */ "(forall mk_(n, x):(nat1 * nat1) &\n (not (n < 2) =>\n (let lhs = id3(mk_(n, x)), rhs = id3(mk_((n - 1), (x - 1))) in if lhs.#1 <> rhs.#1 then lhs.#1 > rhs.#1 else lhs.#2 > rhs.#2)))\n",
/* 81 */ "1 in set dom m\n",
/* 82 */ "1 in set dom m\n",
/* 83 */ "2 in set dom m\n",
/* 84 */ "3 in set dom m\n",
/* 85 */ "while (x > 0) do ...\n",
/* 86 */ "After iv := (iv + 1) (iv < 10)\n"
};

public void testPOG() throws Exception
Expand All @@ -177,7 +177,7 @@ public void testPOG() throws Exception

for (ProofObligation po: polist)
{
Console.out.println(++i + " \"" + po.value.replaceAll("\n", "\\\\n") + "\",");
Console.out.println("/* " + ++i + " */ \"" + po.value.replaceAll("\n", "\\\\n") + "\",");
assertTrue("PO type checked failed", !po.isCheckable || po.getCheckedExpression() != null);
}

Expand Down

0 comments on commit 5cd1063

Please sign in to comment.