tweak non-det var from NaN

AliveToolkit · Sep 20, 2023 · 66bb3bc · 66bb3bc
1 parent 63fa306
commit 66bb3bc
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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);