diff options
Diffstat (limited to 'src/util/resource_manager.h')
| -rw-r--r-- | src/util/resource_manager.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index e49b27286..c84bed38d 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -91,11 +91,11 @@ class CVC4_PUBLIC ResourceManager { /** The amount of resource used. */ uint64_t d_cumulativeResourceUsed; - /** The ammount of resource used during this call. */ + /** The amount of resource used during this call. */ uint64_t d_thisCallResourceUsed; /** - * The ammount of resource budget for this call (min between per call + * The amount of resource budget for this call (min between per call * budget and left-over cumulative budget. */ uint64_t d_thisCallTimeBudget; |