Fix bug related to sort inference + subtypes. (#1125)

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index 73a50bc7acc521f5f7553c6d43a5964cad0efd06..b469ac9d0e2daf2d3b566af130b5c7109c2ba44a 100644 (file)
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -540,7 +540,8 @@ TypeNode SortInference::getTypeForId( int t ){
 }
 
 Node SortInference::getNewSymbol( Node old, TypeNode tn ){
-  if( tn.isNull() || tn==old.getType() ){
+  // if no sort was inferred for this node, return original
+  if( tn.isNull() || tn.isComparableTo( old.getType() ) ){
     return old;
   }else if( old.isConst() ){
     //must make constant of type tn

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index dbff6cff1b4492e9870a8c860da259479eafddcc..5000be7a2232d28a9e18ce49eba782090a97f073 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -70,7 +70,8 @@ SMT2_TESTS = \
        hung13sdk_output2.smt2 \
        declare-funs.smt2 \
        declare-fun-is-match.smt2 \
-       non-fatal-errors.smt2
+       non-fatal-errors.smt2 \
+       sqrt2-sort-inf-unk.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \

diff --git a/test/regress/regress0/sqrt2-sort-inf-unk.smt2 b/test/regress/regress0/sqrt2-sort-inf-unk.smt2
new file mode 100644 (file)
index 0000000..f4b1502
--- /dev/null
+++ b/test/regress/regress0/sqrt2-sort-inf-unk.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --sort-inference
+; EXPECT: unknown
+(set-logic QF_NRA)
+(declare-fun x () Real)
+(assert (= (* x x) 2.0))
+(check-sat)