summaryrefslogtreecommitdiff
path: root/examples
diff options
context:
space:
mode:
authormakaimann <makaim@stanford.edu>2017-01-11 13:47:06 -0800
committermakaimann <makaim@stanford.edu>2017-01-11 13:47:06 -0800
commit16d251144cfe273e599f3d95c6dffd587a5bc511 (patch)
tree4170dee30065700e776e6c7e2e6bf146c12389e9 /examples
parent13dee9ff9189134158ff21524e7ecc73dcdce971 (diff)
Proposed fix for bug 702. Checks to make sure the Expr's operator is not of kind BUILTIN before passing to prefixPrintGetValue()
Diffstat (limited to 'examples')
-rw-r--r--examples/api/combination.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index f9b18f707..a874c4488 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback