summaryrefslogtreecommitdiff
path: root/examples/api/sets-new.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'examples/api/sets-new.cpp')
-rw-r--r--examples/api/sets-new.cpp8
1 files changed, 4 insertions, 4 deletions
diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
index 2ca3db9d2..21ef925df 100644
--- a/examples/api/sets-new.cpp
+++ b/examples/api/sets-new.cpp
@@ -52,8 +52,8 @@ int main()
Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
- cout << "CVC4 reports: " << theorem << " is "
- << slv.checkValidAssuming(theorem) << "." << endl;
+ cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
+ << "." << endl;
}
// Verify emptset is a subset of any set
@@ -63,8 +63,8 @@ int main()
Term theorem = slv.mkTerm(SUBSET, emptyset, A);
- cout << "CVC4 reports: " << theorem << " is "
- << slv.checkValidAssuming(theorem) << "." << endl;
+ cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
+ << "." << endl;
}
// Find me an element in {1, 2} intersection {2, 3}, if there is one.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback