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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1a35c99019301284203e64f4c2a109eeb6aba565..65dae6b8f4c1dbbebe645e8ba95adc85bf9906e1 100644 (file)
--- 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 9881b3e72a15f3cb0ced71c178c4805eb8715698..9fb58156582d789b99a976f20d88fca9e431d22f 100644 (file)
--- 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 (file)
index 0000000..9599b6e
--- /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)