From 75b75bf39b28c6158d79dd12e6bc1034b2c4db36 Mon Sep 17 00:00:00 2001
From: David Chemouil <david.chemouil+git@onera.fr>
Date: Thu, 3 Oct 2024 17:23:04 +0200
Subject: [PATCH 1/2] follow A. Griggio's suggestions to remove multiple lassos
 in traces

---
 res/nusmv-default-bmc-script.scr |  4 ++--
 res/nusmv-default-script.scr     |  2 +-
 res/nuxmv-default-bmc-script.scr |  4 ++--
 res/nuxmv-default-script.scr     | 10 +++-------
 4 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/res/nusmv-default-bmc-script.scr b/res/nusmv-default-bmc-script.scr
index 8f461c7..a3a977e 100644
--- a/res/nusmv-default-bmc-script.scr
+++ b/res/nusmv-default-bmc-script.scr
@@ -1,5 +1,5 @@
 set default_trace_plugin 1;
 set on_failure_script_quits 1;
 go_bmc;
-check_ltlspec_bmc_inc;
-quit -x
+check_ltlspec_sbmc_inc;
+quit -x
\ No newline at end of file
diff --git a/res/nusmv-default-script.scr b/res/nusmv-default-script.scr
index 8a37ca5..09fe888 100644
--- a/res/nusmv-default-script.scr
+++ b/res/nusmv-default-script.scr
@@ -5,4 +5,4 @@ flatten_hierarchy;
 encode_variables;
 build_model;
 check_ltlspec;
-quit -x
+quit -x
\ No newline at end of file
diff --git a/res/nuxmv-default-bmc-script.scr b/res/nuxmv-default-bmc-script.scr
index 8f461c7..a3a977e 100644
--- a/res/nuxmv-default-bmc-script.scr
+++ b/res/nuxmv-default-bmc-script.scr
@@ -1,5 +1,5 @@
 set default_trace_plugin 1;
 set on_failure_script_quits 1;
 go_bmc;
-check_ltlspec_bmc_inc;
-quit -x
+check_ltlspec_sbmc_inc;
+quit -x
\ No newline at end of file
diff --git a/res/nuxmv-default-script.scr b/res/nuxmv-default-script.scr
index 2bffe6a..752efe4 100644
--- a/res/nuxmv-default-script.scr
+++ b/res/nuxmv-default-script.scr
@@ -1,9 +1,5 @@
 set default_trace_plugin 1;
 set on_failure_script_quits 1;
-read_model;
-flatten_hierarchy;
-build_flat_model;
-encode_variables;
-build_boolean_model;
-check_ltlspec_ic3;
-quit -x
+go_msat;
+check_ltlspec_ic3 -i;
+quit -x
\ No newline at end of file

From 4ee682eed13a99a6a7606c9e2576b246ccaaadd2 Mon Sep 17 00:00:00 2001
From: David Chemouil <david.chemouil+git@onera.fr>
Date: Thu, 3 Oct 2024 17:27:00 +0200
Subject: [PATCH 2/2] release 1.2.0

---
 CHANGES.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 126bbdc..1274f5d 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,6 @@
+### 1.2.0 (2024-10-03)
+- fix bug: several lassos in some SMV traces. The BMC algorithm now is now "sbmc_inc" and the complete algorithm is (for nuXmv) "ic3 -i".
+
 ### 1.1.1 (2024-09-27)
 - fix bug: some arithmetic auxiliaries were absent from the generated SMV file