Proposed fix for bug 702. Checks to make sure the Expr's operator is not of kind...
authormakaimann <makaim@stanford.edu>
Wed, 11 Jan 2017 21:47:06 +0000 (13:47 -0800)
committermakaimann <makaim@stanford.edu>
Wed, 11 Jan 2017 21:47:06 +0000 (13:47 -0800)
examples/api/combination.cpp

index f9b18f7070f089685125d1e5f3e07c8da537325f..a874c4488cf31847c010905dc844d24f4d560415 100644 (file)
@@ -28,7 +28,7 @@ void prefixPrintGetValue(SmtEngine& smt, Expr e, int level = 0){
   for(int i = 0; i < level; ++i){ cout << '-'; }
   cout << "smt.getValue(" << e << ") -> " << smt.getValue(e) << endl;
 
-  if(e.hasOperator()){
+  if(e.hasOperator() && e.getOperator().getKind() != kind::BUILTIN){
     prefixPrintGetValue(smt, e.getOperator(), level + 1);
   }