summaryrefslogtreecommitdiff
path: root/src/prop/prop_engine.h
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2010-11-15 23:51:38 +0000
committerTim King <taking@cs.nyu.edu>2010-11-15 23:51:38 +0000
commitda6e14331b883dba0e48bc9879f611376e30bf36 (patch)
treec278574871b64bd8af2332e508e23d5a53dbc1e3 /src/prop/prop_engine.h
parent5e5956d492ab18b5b4d4bb51117ac760867a525d (diff)
Changes to Solver and PropEngine to support lemmasOnDemand during solve but not yet in d_checkSat.
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r--src/prop/prop_engine.h1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index c0483e943..b43c2d859 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -103,7 +103,6 @@ public:
* @param node the formula to assert
*/
void assertLemma(TNode node);
- void assertSafeLemma(TNode node);
/**
* Checks the current context for satisfiability.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback