From 66bb3bc3d6ce06fbb3b47104eb331cd243408fad Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Wed, 20 Sep 2023 11:26:31 +0100
Subject: [PATCH] tweak non-det var from NaN

---
 ir/state.cpp | 4 ++++
 ir/state.h   | 1 +
 ir/type.cpp  | 2 +-
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/ir/state.cpp b/ir/state.cpp
index 3bed233d9..7fa02d75b 100644
--- a/ir/state.cpp
+++ b/ir/state.cpp
@@ -1177,6 +1177,10 @@ void State::addQuantVar(const expr &var) {
   quantified_vars.emplace(var);
 }
 
+void State::addNonDetVar(const expr &var) {
+  nondet_vars.emplace(var);
+}
+
 expr State::getFreshNondetVar(const char *prefix, const expr &type) {
   expr var = expr::mkFreshVar(prefix, type);
   nondet_vars.emplace(var);
diff --git a/ir/state.h b/ir/state.h
index f20b665f0..ac2b924d1 100644
--- a/ir/state.h
+++ b/ir/state.h
@@ -262,6 +262,7 @@ class State {
 
   smt::expr getFreshNondetVar(const char *prefix, const smt::expr &type);
   void addQuantVar(const smt::expr &var);
+  void addNonDetVar(const smt::expr &var);
   void addFnQuantVar(const smt::expr &var);
   void addUndefVar(smt::expr &&var);
   auto& getUndefVars() const { return undef_vars; }
diff --git a/ir/type.cpp b/ir/type.cpp
index 6d7463555..dafb9f0c5 100644
--- a/ir/type.cpp
+++ b/ir/type.cpp
@@ -470,7 +470,7 @@ expr FloatType::fromFloat(State &s, const expr &fp, unsigned nary,
   expr nan = var.sign().concat(expr::mkInt(-1, exp_bits)).concat(fraction);
   assert(isNaNInt(nan));
 
-  s.addQuantVar(std::move(choice_var));
+  s.addNonDetVar(std::move(choice_var));
   s.addPre(std::move(pre));
 
   return expr::mkIf(isnan, nan, val);