From 76fb043babdb8472147bc6cf2fbe7bb7d680456a Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 10 Sep 2024 11:25:25 +0200
Subject: [PATCH] Fix evaluation of goals

---
 CHANGES.md                     | 10 ++++++++++
 src/model/loop.ml              | 15 +++++++--------
 tests/model/goals/dune         | 21 +++++++++++++++++++++
 tests/model/goals/flags.dune   |  0
 tests/model/goals/foo.ae       |  7 +++++++
 tests/model/goals/foo.expected |  0
 tests/model/goals/foo.rsmt2    |  2 ++
 tools/gentests.ml              |  2 +-
 8 files changed, 48 insertions(+), 9 deletions(-)
 create mode 100644 tests/model/goals/dune
 create mode 100644 tests/model/goals/flags.dune
 create mode 100644 tests/model/goals/foo.ae
 create mode 100644 tests/model/goals/foo.expected
 create mode 100644 tests/model/goals/foo.rsmt2

diff --git a/CHANGES.md b/CHANGES.md
index 529246ec4..6ad858cb8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,4 +1,14 @@
 
+next
+----
+
+### Models
+
+- Fix a bug where the condition on evaluated goals was incorrect.
+  This should not affect any current use, since only SMT-LIB2 model
+  verification is supported and it does not have goals.
+
+
 v0.10
 -----
 
diff --git a/src/model/loop.ml b/src/model/loop.ml
index 384905936..c20f01b9e 100644
--- a/src/model/loop.ml
+++ b/src/model/loop.ml
@@ -112,10 +112,10 @@ let bad_model =
         match kind with
         | `Hyp ->
           Format.fprintf fmt "This hypothesis/assertion evaluates to false"
-        | `Goals evaluated_goals ->
+        | `Goal true_goal ->
           Format.fprintf fmt
-            "@[<v>All of the goals at the following locations evaluated to false:@ %a@]"
-            Fmt.(list pp_located) evaluated_goals
+            "@[<v>The goal at the following location evaluated to true:@ %a@]"
+            pp_located true_goal
         | `Clause ->
           Format.fprintf fmt "This assumed clause evaluates to false")
     ~name:"Incorrect model" ()
@@ -686,11 +686,10 @@ module Make
             let _ = eval_acc_direct ~reraise:false st model delayed evaluated_goals acc in
             assert false
         end else begin
-          (* **3** Lastly check that at least one goal evaluated to "true" *)
-          match evaluated_goals with
-          | [] -> st
-          | l when List.exists (fun { contents; _ } -> contents) l -> st
-          | l -> State.error ~file ~loc st bad_model (`Goals l)
+          (* **3** Lastly check that all goals evaluated to "false" *)
+          match List.find_opt (fun { contents; _ } -> contents) evaluated_goals with
+          | None -> st
+          | Some g -> State.error ~file ~loc st bad_model (`Goal g)
         end
       | _ -> st
     in
diff --git a/tests/model/goals/dune b/tests/model/goals/dune
new file mode 100644
index 000000000..aa020504f
--- /dev/null
+++ b/tests/model/goals/dune
@@ -0,0 +1,21 @@
+; File auto-generated by gentests.ml
+
+; Auto-generated part begin
+; Test for foo.ae
+; Full mode test
+
+(rule
+   (target  foo.full)
+   (deps    (:response foo.rsmt2) (:input foo.ae))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff foo.expected foo.full)))
+
+
+; Auto-generated part end
diff --git a/tests/model/goals/flags.dune b/tests/model/goals/flags.dune
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/model/goals/foo.ae b/tests/model/goals/foo.ae
new file mode 100644
index 000000000..147b90e09
--- /dev/null
+++ b/tests/model/goals/foo.ae
@@ -0,0 +1,7 @@
+
+logic x : int
+
+goal g : false
+
+
+
diff --git a/tests/model/goals/foo.expected b/tests/model/goals/foo.expected
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/model/goals/foo.rsmt2 b/tests/model/goals/foo.rsmt2
new file mode 100644
index 000000000..c60162349
--- /dev/null
+++ b/tests/model/goals/foo.rsmt2
@@ -0,0 +1,2 @@
+sat
+()
diff --git a/tools/gentests.ml b/tools/gentests.ml
index 688d75aff..8425c038a 100644
--- a/tools/gentests.ml
+++ b/tools/gentests.ml
@@ -16,7 +16,7 @@ let expected_of_problem file =
 
 let response_of_problem file =
   match Filename.extension file with
-  | ".smt2" -> Some (Filename.chop_extension file ^ ".rsmt2")
+  | ".smt2" | ".ae" -> Some (Filename.chop_extension file ^ ".rsmt2")
   | _ -> None
 
 let supports_incremental file =