cprover
|
Go to the source code of this file.
Functions | |
static bool | cannot_be_neg (const exprt &expr) |
Runs a solver instance to verify whether an expression can only be. More... | |
|
static |
Runs a solver instance to verify whether an expression can only be.
expr | the expression to check for negativity |
expr < 0
is unsatisfiable, false otherwise Definition at line 18 of file string_constraint.cpp.
References decision_proceduret::D_UNSATISFIABLE, from_integer(), solver(), and exprt::type().
Referenced by string_constraintt::string_constraintt().