basic swap test

Fault-lang · Mar 23, 2023 · 02fc31a · 02fc31a
1 parent 64d3e6c
commit 02fc31a
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/smt/testdata/swaps.fspec b/smt/testdata/swaps.fspec
@@ -16,4 +16,5 @@ for 2 run {
         s2.v = 20;
     f2 = new f1;
         f2.target = s2;
+    f2.fn;
 }
diff --git a/smt/testdata/swaps.smt2 b/smt/testdata/swaps.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_NRA)(declare-fun swaps_s2_v_0 () Real)
+(declare-fun swaps_f2_target_v_0 () Real)
+(declare-fun swaps_f2_target_v_1 () Real)
+(declare-fun swaps_f2_target_v_2 () Real)
+(assert (= swaps_s2_v_0 20.0))
+(assert (= swaps_f2_target_v_0 20.0))
+(assert (= swaps_f2_target_v_1 (+ swaps_f2_target_v_0 2.0)))
+(assert (= swaps_f2_target_v_2 (+ swaps_f2_target_v_1 2.0)))