File tree Expand file tree Collapse file tree 3 files changed +9
-10
lines changed Expand file tree Collapse file tree 3 files changed +9
-10
lines changed Original file line number Diff line number Diff line change @@ -278,7 +278,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
278
278
return m_context.mkExpr (CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
279
279
}
280
280
281
- smtAssert (false , " " );
281
+ smtAssert (false );
282
282
}
283
283
catch (CVC4::TypeCheckingException const & _e)
284
284
{
@@ -289,7 +289,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
289
289
smtAssert (false , _e.what ());
290
290
}
291
291
292
- smtAssert (false , " " );
292
+ smtAssert (false );
293
293
294
294
// FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794)
295
295
throw exception ();
Original file line number Diff line number Diff line change @@ -264,14 +264,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
264
264
return constructor (args);
265
265
}
266
266
267
- smtAssert (false , " " );
267
+ smtAssert (false );
268
268
}
269
269
catch (z3::exception const & _e)
270
270
{
271
271
smtAssert (false , _e.msg ());
272
272
}
273
273
274
- smtAssert (false , " " );
274
+ smtAssert (false );
275
275
276
276
// FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794)
277
277
throw exception ();
@@ -382,7 +382,7 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
382
382
)
383
383
return Expression (_expr.decl ().name ().str (), arguments, fromZ3Sort (_expr.get_sort ()));
384
384
385
- smtAssert (false , " " );
385
+ smtAssert (false );
386
386
387
387
// FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794)
388
388
throw exception ();
Original file line number Diff line number Diff line change @@ -1637,7 +1637,7 @@ ASTPointer<Statement> Parser::parseSimpleStatement(ASTPointer<ASTString> const&
1637
1637
return parseExpressionStatement (_docString, nodeFactory.createNode <TupleExpression>(components, false ));
1638
1638
}
1639
1639
default :
1640
- solAssert (false , " " );
1640
+ solAssert (false );
1641
1641
}
1642
1642
}
1643
1643
else
@@ -1650,7 +1650,7 @@ ASTPointer<Statement> Parser::parseSimpleStatement(ASTPointer<ASTString> const&
1650
1650
case LookAheadInfo::Expression:
1651
1651
return parseExpressionStatement (_docString, expressionFromIndexAccessStructure (iap));
1652
1652
default :
1653
- solAssert (false , " " );
1653
+ solAssert (false );
1654
1654
}
1655
1655
}
1656
1656
@@ -1661,9 +1661,8 @@ ASTPointer<Statement> Parser::parseSimpleStatement(ASTPointer<ASTString> const&
1661
1661
bool Parser::IndexAccessedPath::empty () const
1662
1662
{
1663
1663
if (!indices.empty ())
1664
- {
1665
- solAssert (!path.empty (), " " );
1666
- }
1664
+ solAssert (!path.empty ());
1665
+
1667
1666
return path.empty () && indices.empty ();
1668
1667
}
1669
1668
You can’t perform that action at this time.
0 commit comments