diff options
| -rw-r--r-- | src/theory/sort_inference.cpp | 3 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sqrt2-sort-inf-unk.smt2 | 6 |
3 files changed, 10 insertions, 2 deletions
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 73a50bc7a..b469ac9d0 100644 --- 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 dbff6cff1..5000be7a2 100644 --- 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 index 000000000..f4b15020a --- /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) |