Improve test.

gebner · gebner · commit 227fa99393b1 · 2026-03-03T18:29:06.000Z
diff --git a/test/antiquot.c b/test/antiquot.c
@@ -1,7 +1,8 @@
 #include "c2pulse.h"
 
 void test_rvalue_antiquot(int *x)
-    _ensures((_slprop) _inline_pulse(pure ($(*x) = $(*x))))
+    _ensures((_slprop) _inline_pulse(pure (Int32.v $(*x) > 0)))
 {
-    return;
+    _assert((_slprop) _inline_pulse($&(x) |-> $(x)));
+    *x = 6 + 7;
 }

Original file line number	Diff line number	Diff line change
`@@ -1,7 +1,8 @@`
`1`	`1`	`#include "c2pulse.h"`
`2`	`2`
`3`	`3`	`void test_rvalue_antiquot(int *x)`
`4`		`- _ensures((_slprop) _inline_pulse(pure ($(x) = $(x))))`
	`4`	`+ _ensures((_slprop) _inline_pulse(pure (Int32.v $(*x) > 0)))`
`5`	`5`	`{`
`6`		`- return;`
	`6`	`+ _assert((_slprop) _inline_pulse($&(x) \|-> $(x)));`
	`7`	`+ *x = 6 + 7;`
`7`	`8`	`}`