From 38555ee66cdb84de00d8dc27b346ec077452b093 Mon Sep 17 00:00:00 2001 From: yuleisui Date: Thu, 13 Aug 2026 21:44:00 +1000 Subject: [PATCH 1/3] update Lab-Exercise-3 --- Lab-Exercise-3/CPP/AEMgr.cpp | 24 +++++++++++++++--------- Lab-Exercise-3/Python/AEMgr.ipynb | 24 +++++++++++++++--------- 2 files changed, 30 insertions(+), 18 deletions(-) diff --git a/Lab-Exercise-3/CPP/AEMgr.cpp b/Lab-Exercise-3/CPP/AEMgr.cpp index c00f6b0..e25a619 100644 --- a/Lab-Exercise-3/CPP/AEMgr.cpp +++ b/Lab-Exercise-3/CPP/AEMgr.cpp @@ -203,15 +203,21 @@ namespace SVF { } AEState AbstractExecutionMgr::test6() { - // int main(int argv) { // argv is an interval [4, 10] - // int a; - // int b; - // a = argv + 1; - // b = 5; - // if(a > 10) - // b = a; - // assert(b>=5); - // } + // int main(int argv) { // argv is [4, 10] + // int a; + // int b; + // a = argv + 1; + // b = 5; + // + // if (a > 10) { + // b = a; + // if (a <= 8) + // b = 100; + // } + // + // assert(b >= 5); + // } + AEState as; NodeID a = getNodeID("a"); NodeID b = getNodeID("b"); diff --git a/Lab-Exercise-3/Python/AEMgr.ipynb b/Lab-Exercise-3/Python/AEMgr.ipynb index e1bd024..134ec08 100755 --- a/Lab-Exercise-3/Python/AEMgr.ipynb +++ b/Lab-Exercise-3/Python/AEMgr.ipynb @@ -849,7 +849,7 @@ }, { "cell_type": "code", - "execution_count": 88, + "execution_count": null, "id": "d221d14ac9cf5320", "metadata": { "collapsed": false, @@ -883,15 +883,21 @@ "\n", "'''\n", "// C source code\n", - " int main(int argv) { // argv is an interval [4, 10]\n", - " int a;\n", - " int b;\n", - " a = argv + 1;\n", - " b = 5;\n", - " if (a > 10)\n", - " b = a;\n", - " assert(b >= 5);\n", + "int main(int argv) { // argv is an interval [4, 10]\n", + " int a;\n", + " int b;\n", + " a = argv + 1;\n", + " b = 5;\n", + "\n", + " if (a > 10) {\n", + " b = a;\n", + "\n", + " if (a <= 8) // infeasible after refining a > 10\n", + " b = 0;\n", " }\n", + "\n", + " assert(b >= 5);\n", + "}\n", "'''\n", "def test6():\n", " mgr = AbstractExecutionMgr()\n", From df3b4bf5bcf97bffb40f056f8c9ea44b7457ab25 Mon Sep 17 00:00:00 2001 From: Yulei Sui <7608399+yuleisui@users.noreply.github.com> Date: Fri, 14 Aug 2026 22:17:06 +1000 Subject: [PATCH 2/3] Update Lab-Exercise-3/Python/AEMgr.ipynb Co-authored-by: Mohamad Barbar --- Lab-Exercise-3/Python/AEMgr.ipynb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lab-Exercise-3/Python/AEMgr.ipynb b/Lab-Exercise-3/Python/AEMgr.ipynb index 134ec08..a8f4599 100755 --- a/Lab-Exercise-3/Python/AEMgr.ipynb +++ b/Lab-Exercise-3/Python/AEMgr.ipynb @@ -892,7 +892,7 @@ " if (a > 10) {\n", " b = a;\n", "\n", - " if (a <= 8) // infeasible after refining a > 10\n", + " if (a <= 8)\n", " b = 0;\n", " }\n", "\n", From 63e804f7bec98100c4c1abd82a45dcfa74f1ee4e Mon Sep 17 00:00:00 2001 From: Yulei Sui <7608399+yuleisui@users.noreply.github.com> Date: Fri, 14 Aug 2026 22:17:34 +1000 Subject: [PATCH 3/3] Update Lab-Exercise-3/CPP/AEMgr.cpp Co-authored-by: Mohamad Barbar --- Lab-Exercise-3/CPP/AEMgr.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lab-Exercise-3/CPP/AEMgr.cpp b/Lab-Exercise-3/CPP/AEMgr.cpp index e25a619..013bc6f 100644 --- a/Lab-Exercise-3/CPP/AEMgr.cpp +++ b/Lab-Exercise-3/CPP/AEMgr.cpp @@ -212,7 +212,7 @@ namespace SVF { // if (a > 10) { // b = a; // if (a <= 8) - // b = 100; + // b = 0; // } // // assert(b >= 5);