From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 28 Nov 2017 01:23:49 +0000 (-0600)
Subject: Fix models for --solve-real-as-int. (#1371)
X-Git-Tag: cvc5-1.0.0~5452
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d552ca179b8723a93c6e0dae61242ceb1ccaa717;p=cvc5.git

Fix models for --solve-real-as-int. (#1371)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1a35c9901..65dae6b8f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2805,6 +2805,8 @@ Node SmtEnginePrivate::realToInt(TNode n, NodeMap& cache, std::vector< Node >& v
         if( !n.getType().isInteger() ){
           ret = NodeManager::currentNM()->mkSkolem("__realToInt_var", NodeManager::currentNM()->integerType(), "Variable introduced in realToInt pass");
           var_eq.push_back( n.eqNode( ret ) );
+          TheoryModel* m = d_smt.d_theoryEngine->getModel();
+          m->addSubstitution(n,ret);
         }
       }
     }
diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index 9881b3e72..9fb581565 100644
--- a/test/regress/regress0/nl/Makefile.am
+++ b/test/regress/regress0/nl/Makefile.am
@@ -51,6 +51,7 @@ TESTS =	\
   div-mod-partial.smt2 \
   all-logic.smt2 \
   sqrt-problem-1.smt2 \
+  real-as-int.smt2 \
   nta/bad-050217.smt2 \
   nta/cos-bound.smt2 \
   nta/cos-sig-value.smt2 \
diff --git a/test/regress/regress0/nl/real-as-int.smt2 b/test/regress/regress0/nl/real-as-int.smt2
new file mode 100644
index 000000000..9599b6e6b
--- /dev/null
+++ b/test/regress/regress0/nl/real-as-int.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-real-as-int 
+; EXPECT: sat
+(set-logic QF_NRA)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (= (* a a) 4))
+(assert (= (* b b) 0))
+(assert (= (+ (* a a) (* b b)) 4))
+(check-sat)